# HG changeset patch
# User wenzelm
# Date 1262095211 -3600
# Node ID 211ac6c4d4c9e2e4e45240becd6e65595a551b26
# Parent  c7417fb4311229aebfe5472114ec971f1b89e652
tuned;

diff -r c7417fb43112 -r 211ac6c4d4c9 src/Tools/jEdit/src/jedit/document_view.scala
--- 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)