# HG changeset patch
# User immler
# Date 1353511954 -3600
# Node ID e2c08f20d00efc1feb47b06f0ea8a5f45cac0d6c
# Parent  ab5272955b3b3d071eb7ac9f4a894ab7dfdc9ac7
included abbrev in tooltip

diff -r ab5272955b3b -r e2c08f20d00e src/Tools/jEdit/src/symbols_dockable.scala
--- 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 {