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.
included abbrev in tooltip
authorimmler
Wed, 21 Nov 2012 16:32:34 +0100
changeset 50155 e2c08f20d00e
parent 50154 ab5272955b3b
child 50156 12a65e2ee296
included abbrev in tooltip
src/Tools/jEdit/src/symbols_dockable.scala file | annotate | diff | comparison | revisions 
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Wed Nov 21 16:21:16 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Wed Nov 21 16:32:34 2012 +0100
@@ -33,7 +33,9 @@
       new Font(Symbol.fonts.getOrElse(symbol, Isabelle.font_family()),
         Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
     action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus }
-    tooltip = symbol + " - " + get_name(dec)
+    tooltip = symbol +
+      (if (Symbol.abbrevs.isDefinedAt(symbol)) " abbrev: " + Symbol.abbrevs(symbol) else "") +
+      " - " + get_name(dec)
   }
 
   val group_tabs: TabbedPane = new TabbedPane {
isabelle