# HG changeset patch
# User wenzelm
# Date 1333813760 -7200
# Node ID 6a08fd7a607171253098afd0f71d5d08e0b9b1f4
# Parent  d78fbe1915445a608a880e2114ba8a8549ca9cea
tuned imports;

diff -r d78fbe191544 -r 6a08fd7a6071 src/Tools/jEdit/src/document_view.scala
--- 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}