--- a/src/Tools/jEdit/src/symbols_dockable.scala Sat Nov 24 15:49:43 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Sat Nov 24 16:13:21 2012 +0100
@@ -21,10 +21,7 @@
val searchspace =
for ((group, symbols) <- Symbol.groups; sym <- symbols)
- yield (sym, (sym.toLowerCase + get_name(Symbol.decode(sym)).toLowerCase))
-
- def get_name(c: String): String =
- if (c.length >= 1) Character.getName(c.codePointAt(0)) else "??"
+ yield (sym, sym.toLowerCase)
private class Symbol_Component(val symbol: String) extends Button
{
@@ -33,9 +30,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 +
- (if (Symbol.abbrevs.isDefinedAt(symbol)) " abbrev: " + Symbol.abbrevs(symbol) else "") +
- " - " + get_name(dec)
+ tooltip =
+ symbol +
+ (if (Symbol.abbrevs.isDefinedAt(symbol)) " abbrev: " + Symbol.abbrevs(symbol) else "")
}
val group_tabs: TabbedPane = new TabbedPane {