proper multi-line tooltip;
authorwenzelm
Mon, 10 Sep 2012 19:56:08 +0200
changeset 49248 bff772033a97
parent 49247 ffd9ad9dc35b
child 49249 c763444b34ad
proper multi-line tooltip;
src/Tools/jEdit/src/isabelle_logic.scala
src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala	Mon Sep 10 19:49:30 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Mon Sep 10 19:56:08 2012 +0200
@@ -53,7 +53,7 @@
       component.listenTo(component.selection)
       component.reactions += { case SelectionChanged(_) => component.save() }
     }
-    component.tooltip = Isabelle.options.value.check_name("jedit_logic").print
+    component.tooltip = Isabelle.tooltip(Isabelle.options.value.check_name("jedit_logic").print)
     component
   }
 
--- a/src/Tools/jEdit/src/jedit_options.scala	Mon Sep 10 19:49:30 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Mon Sep 10 19:56:08 2012 +0200
@@ -58,7 +58,7 @@
         text_area
       }
     component.load()
-    component.tooltip = opt.print
+    component.tooltip = Isabelle.tooltip(opt.print)
     component
   }
 }