# HG changeset patch
# User wenzelm
# Date 1246044050 -7200
# Node ID 313fcd844129128fbee6ea95f1f2f1fc29d38572
# Parent  7124433be8beeeb8233058d097e9361f8545799f
recovered Isabelle font -- deriveFont(Int) refers to style, not size!

diff -r 7124433be8be -r 313fcd844129 src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Fri Jun 26 20:54:42 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Fri Jun 26 21:20:50 2009 +0200
@@ -90,8 +90,8 @@
   def set_font(size: Int)
   {
     font = Font.createFont(Font.TRUETYPE_FONT,
-        new FileInputStream(Isabelle.system.platform_path("~~/lib/fonts/IsabelleMono.ttf"))).
-      deriveFont(Font.PLAIN, size max 1)
+        Isabelle.system.platform_file("~~/lib/fonts/IsabelleMono.ttf")).
+      deriveFont(Font.PLAIN, (size max 1).toFloat)
     font_changed.event(font)
   }