tuned;

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Mon Dec 28 22:04:45 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Dec 29 15:00:11 2009 +0100
@@ -192,6 +192,8 @@
     private val WIDTH = 10
     private val HEIGHT = 2
 
+    setPreferredSize(new Dimension(WIDTH, 0))
+
     setRequestFocusEnabled(false)
 
     addMouseListener(new MouseAdapter {
@@ -235,8 +237,6 @@
       }
     }
 
-    override def getPreferredSize = new Dimension(WIDTH, 0)
-
     private def line_to_y(line: Int): Int =
       (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)