Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
authorwenzelm
Sat, 19 Apr 2014 19:03:32 +0200
changeset 56622 891d1b8b64fb
parent 56621 798ba1c2da12
child 56623 4675df68450e
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
src/Pure/GUI/gui.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/find_dockable.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/jedit_options.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/sledgehammer_dockable.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/spell_checker.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/symbols_dockable.scala file | annotate | diff | comparison | revisions 
--- a/src/Pure/GUI/gui.scala	Sat Apr 19 18:37:41 2014 +0200
+++ b/src/Pure/GUI/gui.scala	Sat Apr 19 19:03:32 2014 +0200
@@ -137,9 +137,9 @@
 
   /* tooltip with multi-line support */
 
-  def tooltip_lines(lines: List[String]): String =
-    if (lines.isEmpty) null
-    else "<html><pre>" + HTML.encode(cat_lines(lines)) + "</pre></html>"
+  def tooltip_lines(text: String): String =
+    if (text == null || text == "") null
+    else "<html>" + HTML.encode(text) + "</html>"
 
 
   /* screen resolution */
--- a/src/Tools/jEdit/src/find_dockable.scala	Sat Apr 19 18:37:41 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Sat Apr 19 19:03:32 2014 +0200
@@ -106,10 +106,8 @@
 
   private val query_label = new Label("Search criteria:") {
     tooltip =
-      GUI.tooltip_lines(List(
-        "Search criteria for find operation, e.g.",
-        "",
-        "  \"_ = _\" \"op +\" name: Group -name: monoid"))
+      GUI.tooltip_lines(
+        "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
   }
 
   private val query = new Completion_Popup.History_Text_Field("isabelle-find-theorems") {
--- a/src/Tools/jEdit/src/jedit_options.scala	Sat Apr 19 18:37:41 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Sat Apr 19 19:03:32 2014 +0200
@@ -49,7 +49,7 @@
       def load = button.setSelectedColor(Color_Value(string(opt_name)))
       def save = string(opt_name) = Color_Value.print(button.getSelectedColor)
     }
-    component.tooltip = GUI.tooltip_lines(List(opt.print_default))
+    component.tooltip = GUI.tooltip_lines(opt.print_default)
     component
   }
 
@@ -96,7 +96,7 @@
         text_area
       }
     component.load()
-    component.tooltip = GUI.tooltip_lines(List(opt.print_default))
+    component.tooltip = GUI.tooltip_lines(opt.print_default)
     component
   }
 
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Apr 19 18:37:41 2014 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Apr 19 19:03:32 2014 +0200
@@ -137,10 +137,8 @@
 
   private val provers_label = new Label("Provers:") {
     tooltip =
-      GUI.tooltip_lines(List(
-        "Automatic provers as space-separated list, e.g.",
-        "",
-        "  e spass remote_vampire"))
+      GUI.tooltip_lines(
+        "Automatic provers as space-separated list, e.g.\ne spass remote_vampire")
   }
 
   private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
--- a/src/Tools/jEdit/src/spell_checker.scala	Sat Apr 19 18:37:41 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala	Sat Apr 19 19:03:32 2014 +0200
@@ -126,7 +126,7 @@
     }
 
     component.load()
-    component.tooltip = GUI.tooltip_lines(List(opt.print_default))
+    component.tooltip = GUI.tooltip_lines(opt.print_default)
     component
   }
 
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Apr 19 18:37:41 2014 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Apr 19 19:03:32 2014 +0200
@@ -41,7 +41,9 @@
         else text_area.setSelectedText(decoded)
         text_area.requestFocus
       }
-    tooltip = GUI.tooltip_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a))
+    tooltip =
+      GUI.tooltip_lines(
+        cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a)))
   }
 
   private class Reset_Component extends Button
isabelle