# HG changeset patch
# User wenzelm
# Date 1353775614 -3600
# Node ID 8b5a256859af5a474090bd31473b6fe61d8f0a21
# Parent  0d7f0d8fd63bb6b7d94c53b4be5a25fc32c5e8f9
more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;

diff -r 0d7f0d8fd63b -r 8b5a256859af src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 17:12:06 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 17:46:54 2012 +0100
@@ -24,9 +24,13 @@
   private class Symbol_Component(val symbol: String) extends Button
   {
     private val decoded = Symbol.decode(symbol)
+    private val font_size = Isabelle.font_size("jedit_font_scale").round
+
     font =
-      new Font(Symbol.fonts.getOrElse(symbol, Isabelle.font_family()),
-        Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
+      Symbol.fonts.get(symbol) match {
+        case None => Isabelle_System.get_font(size = font_size)
+        case Some(font_family) => Isabelle_System.get_font(family = font_family, size = font_size)
+      }
     action =
       Action(decoded) {
         val text_area = view.getTextArea