# HG changeset patch
# User immler
# Date 1353506006 -3600
# Node ID 164af3238434d9dc883920f33a76cebd204d4ad8
# Parent  5f5e74365f14c3688785decc20de4d3dc0fea9b3
respect font property for symbols

diff -r 5f5e74365f14 -r 164af3238434 src/Tools/jEdit/src/symbols_dockable.scala
--- 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)