src/Tools/jEdit/src/plugin.scala
changeset 43520 cec9b95fa35d
parent 43513 06951ddfc812
child 43643 474745a899ea
--- a/src/Tools/jEdit/src/plugin.scala	Thu Jun 23 14:48:32 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Jun 23 14:52:32 2011 +0200
@@ -9,6 +9,7 @@
 
 import isabelle._
 
+import java.lang.System
 import java.io.{FileInputStream, IOException}
 import java.awt.Font