# 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 {