src/Tools/jEdit/src/document_view.scala

 
 
   /* caret handling */
 
   private val delay_caret_update =
-    Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) {
+    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
       session.caret_focus.event(Session.Caret_Focus)
     }
 
   private val caret_listener = new CaretListener {
     override def caretUpdate(e: CaretEvent) { delay_caret_update.invoke() }

   /* text status overview left of scrollbar */
 
   private object overview extends Text_Overview(this)
   {
     val delay_repaint =
-      Swing_Thread.delay_first(Time.seconds(PIDE.options.real("editor_update_delay"))) { repaint() }
+      Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
   }
 
 
   /* main actor */
 
   private val main_actor = actor {
     loop {
       react {
         case _: Session.Raw_Edits =>
           Swing_Thread.later {
-            overview.delay_repaint.postpone(Time.seconds(PIDE.options.real("editor_input_delay")))
+            overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
           }
 
         case changed: Session.Commands_Changed =>
           val buffer = model.buffer
           Swing_Thread.later {