UI and font size changes.

NEWS

@@ -1,3 +1,6 @@
+1.3.7: April 29, 2008
+ * Several minor font size and other UI changes.
+
 1.3.6: April 28, 2008
  * Can now click "more" link to display more than ten "recent updates".
 

static/css/note.css

@@ -109,3 +109,7 @@ ol li {
   margin-bottom: 0.5em;
   border: 1px solid #999999;
 }
+
+.search_results_summary {
+  font-size: 82%;
+}

static/css/style.css

@@ -741,6 +741,10 @@ img {
   font-weight: normal;
 }
 
+#note_tree_instructions {
+  line-height: 140%;
+}
+
 .new_feature_text {
   font-size: 90%;
   font-weight: bold;

static/js/Wiki.js

@@ -1364,6 +1364,7 @@ Wiki.prototype.display_search_results = function ( result ) {
     }
 
     var summary_span = createDOM( "span" );
+    summary_span.setAttribute( "class", "search_results_summary" );
     summary_span.innerHTML = summary;
 
     appendChildNodes( list,

view/Note_tree_area.py

@@ -28,7 +28,7 @@ class Note_tree_area( Div ):
           Tr( Td(
             ( notebook.name != u"trash" ) and u'To add a note here, click the "options" tab on a note, then "show on startup".' or None,
             id = "note_tree_instructions",
-            class_ = u"small_text link_area_item" + ( ( len( root_notes ) > 0 ) and u" undisplayed" or u"" ),
+            class_ = u"link_area_item" + ( ( len( root_notes ) > 0 ) and u" undisplayed" or u"" ),
           ) ) or None,
           tree_id = "note_tree_root_table",
         ),