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