# HG changeset patch
# User wenzelm
# Date 1260222075 -3600
# Node ID 6ed1b3701459a38293dad0bc4a6c2a9a7d43936e
# Parent  8a630617faa9952dc52c4c092d841d71cb47ee7f
simplified treatment of Isabelle fonts, via Isabelle_System.register_fonts (requires Java 1.6);

diff -r 8a630617faa9 -r 6ed1b3701459 src/Tools/jEdit/src/jedit/OptionPane.scala
--- a/src/Tools/jEdit/src/jedit/OptionPane.scala	Mon Dec 07 22:40:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/OptionPane.scala	Mon Dec 07 22:41:15 2009 +0100
@@ -38,10 +38,6 @@
     Isabelle.Property("logic") = logic
 
     val size = font_size.getValue().asInstanceOf[Int]
-    if (Isabelle.Int_Property("font-size") != size)
-    {
-      Isabelle.Int_Property("font-size") = size
-      Swing_Thread.later { Isabelle.plugin.set_font(size) }
-    }
+    Isabelle.Int_Property("font-size") = size
   }
 }
diff -r 8a630617faa9 -r 6ed1b3701459 src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Mon Dec 07 22:40:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Mon Dec 07 22:41:15 2009 +0100
@@ -84,20 +84,6 @@
 
 class Plugin extends EBPlugin
 {
-  /* Isabelle font */
-
-  var font: Font = null
-  val font_changed = new Event_Bus[Font]
-
-  def set_font(size: Int)
-  {
-    font = Font.createFont(Font.TRUETYPE_FONT,
-        Isabelle.system.platform_file("~~/lib/fonts/IsabelleMono.ttf")).
-      deriveFont(Font.PLAIN, (size max 1).toFloat)
-    font_changed.event(font)
-  }
-
-
   /* event buses */
 
   val state_update = new Event_Bus[Command]
@@ -154,9 +140,10 @@
 
   override def start()
   {
+    Isabelle.plugin = this
     Isabelle.system = new Isabelle_System
-    Isabelle.plugin = this
-    set_font(Isabelle.Int_Property("font-size"))
+    if (!Isabelle.system.register_fonts())
+      System.err.println("Failed to register Isabelle fonts")
   }
 
   override def stop()