diff -r 7700f0e9618c -r 135fd6f2dadd 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() }