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