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.
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
authorwenzelm
Sat, 24 Nov 2012 16:24:39 +0100
changeset 50186 f83cab68c788
parent 50185 820673500454
child 50187 b5a09812abc4
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
src/Tools/jEdit/src/jedit_lib.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/symbols_dockable.scala file | annotate | diff | comparison | revisions 
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 24 16:13:21 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 24 16:24:39 2012 +0100
@@ -47,6 +47,13 @@
     ancestors(component).find(_.isInstanceOf[Frame]).map(_.asInstanceOf[Frame])
 
 
+  /* basic tooltips, with multi-line support */
+
+  def wrap_tooltip(text: String): String =
+    if (text == "") null
+    else "<html><pre>" + HTML.encode(text) + "</pre></html>"
+
+
   /* buffers */
 
   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 16:13:21 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 16:24:39 2012 +0100
@@ -31,8 +31,9 @@
         Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
     action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus }
     tooltip =
-      symbol +
-        (if (Symbol.abbrevs.isDefinedAt(symbol)) " abbrev: " + Symbol.abbrevs(symbol) else "")
+      JEdit_Lib.wrap_tooltip(
+        symbol +
+          (if (Symbol.abbrevs.isDefinedAt(symbol)) "\nabbrev: " + Symbol.abbrevs(symbol) else ""))
   }
 
   val group_tabs: TabbedPane = new TabbedPane {
isabelle