simplified treatment of Isabelle fonts, via Isabelle_System.register_fonts (requires Java 1.6);
--- 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
}
}
--- 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()