# HG changeset patch
# User wenzelm
# Date 1701003747 -3600
# Node ID 212c94edae2b4d39ca3ffbe2e8b508cedaf12d52
# Parent  0da44db32646dc2aa1add8f4fe200e5dd25c95a2
more reactive headless server, in contrast to 15656ad28691 (when "isabelle dump" was important to export AFP content);

diff -r 0da44db32646 -r 212c94edae2b etc/options
--- a/etc/options	Sun Nov 26 13:32:51 2023 +0100
+++ b/etc/options	Sun Nov 26 14:02:27 2023 +0100
@@ -273,10 +273,10 @@
 
 section "Headless Session"
 
-option headless_consolidate_delay : real = 15
+option headless_consolidate_delay : real = 2.0
   -- "delay to consolidate status of command evaluation (execution forks)"
 
-option headless_prune_delay : real = 60
+option headless_prune_delay : real = 30
   -- "delay to prune history (delete old versions)"
 
 option headless_check_delay : real = 0.5
diff -r 0da44db32646 -r 212c94edae2b src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sun Nov 26 13:32:51 2023 +0100
+++ b/src/Doc/System/Server.thy	Sun Nov 26 14:02:27 2023 +0100
@@ -838,6 +838,10 @@
 
   Start a session from the Archive of Formal Proofs:
   @{verbatim [display] \<open>session_start {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
+
+  Start a session with fine-tuning of options:
+  @{verbatim [display] \<open>session_start {"session": "HOL",
+  "options": ["headless_consolidate_delay=0.5", "headless_prune_delay=5"]}\<close>}
 \<close>