diff -r 9b3a8565464d -r 3991a35cd740 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Jan 31 16:13:27 2023 +0100
+++ b/src/Pure/PIDE/session.scala	Tue Jan 31 17:00:33 2023 +0100
@@ -147,6 +147,7 @@
   def prune_delay: Time = session_options.seconds("editor_prune_delay")
   def prune_size: Int = session_options.int("editor_prune_size")
   def update_delay: Time = session_options.seconds("editor_update_delay")
+  def document_delay: Time = session_options.seconds("editor_document_delay")
   def chart_delay: Time = session_options.seconds("editor_chart_delay")
   def syslog_limit: Int = session_options.int("editor_syslog_limit")
   def reparse_limit: Int = session_options.int("editor_reparse_limit")