--- a/src/Tools/jEdit/src/symbols_dockable.scala Wed Nov 21 12:11:21 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Wed Nov 21 14:53:26 2012 +0100
@@ -30,7 +30,7 @@
{
val dec = Symbol.decode(symbol)
font =
- new Font(Isabelle.font_family(),
+ 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 + " - " + get_name(dec)