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