1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Apr 07 17:48:47 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Apr 07 17:49:20 2012 +0200
     1.3 @@ -27,8 +27,7 @@
     1.4  import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
     1.5  import org.gjt.sp.jedit.gui.RolloverButton
     1.6  import org.gjt.sp.jedit.options.GutterOptionPane
     1.7 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter,
     1.8 -  ScrollListener}
     1.9 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    1.10  import org.gjt.sp.jedit.syntax.{SyntaxStyle}
    1.11  
    1.12