src/Tools/jEdit/src/document_view.scala

--- a/src/Tools/jEdit/src/document_view.scala	Thu May 24 21:46:11 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Thu May 24 22:07:00 2012 +0200
@@ -329,7 +329,7 @@
 
   /* text status overview left of scrollbar */
 
-  private val overview = new Text_Overview(this)
+  private object overview extends Text_Overview(this)
   {
     val delay_repaint =
       Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }