# HG changeset patch
# User wenzelm
# Date 1570282494 -7200
# Node ID 15656ad28691822aad11de60d52570f936c87eba
# Parent  d50c8f4f209050f0eb3826df4008b5d0f01b58c3
clarified options -- more scalable;

diff -r d50c8f4f2090 -r 15656ad28691 etc/options
--- a/etc/options	Fri Oct 04 16:34:14 2019 +0200
+++ b/etc/options	Sat Oct 05 15:34:54 2019 +0200
@@ -162,7 +162,7 @@
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
-public option editor_consolidate_delay : real = 3.0
+public option editor_consolidate_delay : real = 2.0
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 public option editor_prune_delay : real = 15
@@ -201,6 +201,12 @@
 
 section "Headless Session"
 
+option headless_consolidate_delay : real = 15
+  -- "delay to consolidate status of command evaluation (execution forks)"
+
+option headless_prune_delay : real = 60
+  -- "delay to prune history (delete old versions)"
+
 option headless_check_delay : real = 0.5
   -- "delay for theory status check during PIDE processing (seconds)"
 
@@ -216,7 +222,7 @@
 option headless_commit_cleanup_delay : real = 60
   -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
 
-option headless_load_limit : int = 0
+option headless_load_limit : int = 100
   -- "limit for loaded theories (0 = unlimited)"
 
 option dump_checkpoint : bool = false
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")