src/Tools/jEdit/src/symbols_dockable.scala
changeset 50155 e2c08f20d00e
parent 50154 ab5272955b3b
child 50185 820673500454
equal deleted inserted replaced
50154:ab5272955b3b 50155:e2c08f20d00e
    31     val dec = Symbol.decode(symbol)
    31     val dec = Symbol.decode(symbol)
    32     font =
    32     font =
    33       new Font(Symbol.fonts.getOrElse(symbol, Isabelle.font_family()),
    33       new Font(Symbol.fonts.getOrElse(symbol, Isabelle.font_family()),
    34         Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
    34         Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
    35     action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus }
    35     action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus }
    36     tooltip = symbol + " - " + get_name(dec)
    36     tooltip = symbol +
       
    37       (if (Symbol.abbrevs.isDefinedAt(symbol)) " abbrev: " + Symbol.abbrevs(symbol) else "") +
       
    38       " - " + get_name(dec)
    37   }
    39   }
    38 
    40 
    39   val group_tabs: TabbedPane = new TabbedPane {
    41   val group_tabs: TabbedPane = new TabbedPane {
    40     pages ++= (for ((group, symbols) <- Symbol.groups) yield
    42     pages ++= (for ((group, symbols) <- Symbol.groups) yield
    41       {
    43       {