src/Tools/jEdit/src/document_view.scala
changeset 43520 cec9b95fa35d
parent 43510 17d431c92575
child 43650 f00da558b78e
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Jun 23 14:48:32 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Jun 23 14:52:32 2011 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4  
     1.5  import scala.actors.Actor._
     1.6  
     1.7 +import java.lang.System
     1.8  import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
     1.9  import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
    1.10    FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}