src/Tools/jEdit/src/document_view.scala

     Swing_Thread.require()
     model.snapshot().node.command_at(text_area.getCaretPosition).map(_._1)
   }
 
   private val delay_caret_update =
-    Swing_Thread.delay_last(session.input_delay) {
+    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("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(Isabelle.session.update_delay) { repaint() }
+      Swing_Thread.delay_first(
+        Time.seconds(Isabelle.options.real("editor_update_delay"))) { repaint() }
   }
 
 
   /* main actor */
 
   private val main_actor = actor {
     loop {
       react {
         case _: Session.Raw_Edits =>
           Swing_Thread.later {
-            overview.delay_repaint.postpone(Isabelle.session.input_delay)
+            overview.delay_repaint.postpone(
+              Time.seconds(Isabelle.options.real("editor_input_delay")))
           }
 
         case changed: Session.Commands_Changed =>
           val buffer = model.buffer
           Swing_Thread.later {