src/Pure/PIDE/document_editor.scala

--- a/src/Pure/PIDE/document_editor.scala	Thu Dec 08 22:11:36 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Thu Dec 08 22:38:03 2022 +0100
@@ -28,8 +28,7 @@
     private val syslog = session.make_syslog()
 
     private def update(text: String = syslog.content()): Unit = show(text)
-    private val delay =
-      Delay.first(session.session_options.seconds("editor_update_delay"), gui = true) { update() }
+    private val delay = Delay.first(session.update_delay, gui = true) { update() }
 
     override def echo(msg: String): Unit = { syslog += msg; delay.invoke() }