diff -r d50c8f4f2090 -r 15656ad28691 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Fri Oct 04 16:34:14 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Sat Oct 05 15:34:54 2019 +0200
@@ -135,6 +135,9 @@
 
     /* options */
 
+    override def consolidate_delay: Time = session_options.seconds("headless_consolidate_delay")
+    override def prune_delay: Time = session_options.seconds("headless_prune_delay")
+
     def default_check_delay: Time = session_options.seconds("headless_check_delay")
     def default_check_limit: Int = session_options.int("headless_check_limit")
     def default_nodes_status_delay: Time = session_options.seconds("headless_nodes_status_delay")