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