more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;

--- 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