src/Tools/jEdit/src/symbols_dockable.scala
changeset 50185 820673500454
parent 50155 e2c08f20d00e
child 50186 f83cab68c788
equal deleted inserted replaced
50184:5a16f42a9b44 50185:820673500454
    19 {
    19 {
    20   private val max_results = 50
    20   private val max_results = 50
    21 
    21 
    22   val searchspace =
    22   val searchspace =
    23     for ((group, symbols) <- Symbol.groups; sym <- symbols)
    23     for ((group, symbols) <- Symbol.groups; sym <- symbols)
    24       yield (sym, (sym.toLowerCase + get_name(Symbol.decode(sym)).toLowerCase))
    24       yield (sym, sym.toLowerCase)
    25 
       
    26   def get_name(c: String): String =
       
    27     if (c.length >= 1) Character.getName(c.codePointAt(0)) else "??"
       
    28 
    25 
    29   private class Symbol_Component(val symbol: String) extends Button
    26   private class Symbol_Component(val symbol: String) extends Button
    30   {
    27   {
    31     val dec = Symbol.decode(symbol)
    28     val dec = Symbol.decode(symbol)
    32     font =
    29     font =
    33       new Font(Symbol.fonts.getOrElse(symbol, Isabelle.font_family()),
    30       new Font(Symbol.fonts.getOrElse(symbol, Isabelle.font_family()),
    34         Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
    31         Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
    35     action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus }
    32     action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus }
    36     tooltip = symbol +
    33     tooltip =
    37       (if (Symbol.abbrevs.isDefinedAt(symbol)) " abbrev: " + Symbol.abbrevs(symbol) else "") +
    34       symbol +
    38       " - " + get_name(dec)
    35         (if (Symbol.abbrevs.isDefinedAt(symbol)) " abbrev: " + Symbol.abbrevs(symbol) else "")
    39   }
    36   }
    40 
    37 
    41   val group_tabs: TabbedPane = new TabbedPane {
    38   val group_tabs: TabbedPane = new TabbedPane {
    42     pages ++= (for ((group, symbols) <- Symbol.groups) yield
    39     pages ++= (for ((group, symbols) <- Symbol.groups) yield
    43       {
    40       {