src/Tools/jEdit/src/jedit/Plugin.scala
changeset 34456 14367c0715e8
parent 34449 57fce8528a22
child 34462 fefbd0421e4e
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Mon Dec 29 20:36:34 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Mon Dec 29 20:43:04 2008 +0100
@@ -14,7 +14,6 @@
 
 import scala.collection.mutable.HashMap
 
-import isabelle.utils.EventSource
 import isabelle.prover.{Prover, Command}
 import isabelle.{IsabelleSystem, Symbol}
 
@@ -55,17 +54,12 @@
   // Isabelle font
 
   var font: Font = null
-  val font_changed = new EventSource[Font]
+  val font_changed = new EventBus[Font]
 
   def set_font(path: String, size: Float) {
-    try {
-      font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)).
-        deriveFont(Font.PLAIN, size)
-      font_changed.fire(font)
-    }
-    catch {
-      case e: IOException =>
-    }
+    font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)).
+      deriveFont(Font.PLAIN, size)
+    font_changed.event(font)
   }