# HG changeset patch
# User wenzelm
# Date 1347299768 -7200
# Node ID bff772033a97b358c876a2c785bec1b9d3baab8a
# Parent  ffd9ad9dc35b44e103ae1760f529aab8eae3d720
proper multi-line tooltip;

diff -r ffd9ad9dc35b -r bff772033a97 src/Tools/jEdit/src/isabelle_logic.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
   }
 
diff -r ffd9ad9dc35b -r bff772033a97 src/Tools/jEdit/src/jedit_options.scala
--- 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
   }
 }