src/Tools/jEdit/src/document_view.scala
changeset 47993 135fd6f2dadd
parent 47392 6a08fd7a6071
child 48921 5d8d409b897e
equal deleted inserted replaced
47992:7700f0e9618c 47993:135fd6f2dadd
   327   }
   327   }
   328 
   328 
   329 
   329 
   330   /* text status overview left of scrollbar */
   330   /* text status overview left of scrollbar */
   331 
   331 
   332   private val overview = new Text_Overview(this)
   332   private object overview extends Text_Overview(this)
   333   {
   333   {
   334     val delay_repaint =
   334     val delay_repaint =
   335       Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }
   335       Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }
   336   }
   336   }
   337 
   337