src/Tools/jEdit/src/html_panel.scala
changeset 43520 cec9b95fa35d
parent 43455 4b4b93672f15
child 43551 07a9cbf2376f
     1.1 --- a/src/Tools/jEdit/src/html_panel.scala	Thu Jun 23 14:48:32 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Thu Jun 23 14:52:32 2011 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 +import java.lang.System
     1.8  import java.io.StringReader
     1.9  import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
    1.10  import java.awt.event.MouseEvent