# HG changeset patch
# User wenzelm
# Date 1353770001 -3600
# Node ID 820673500454d5961af8b1403a4416c1639826bb
# Parent  5a16f42a9b44a8d0fd02af4bf9513e647e38ba65
avoid showing semantic aspects of Unicode -- Isabelle/Scala merely (ab)uses the low-level rendering model (codepoint + font);

diff -r 5a16f42a9b44 -r 820673500454 src/Tools/jEdit/src/symbols_dockable.scala
--- 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 {