equal
deleted
inserted
replaced
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 { |