# HG changeset patch
# User wenzelm
# Date 1569952482 -7200
# Node ID f326596f5752ff9f9a1adae8a430eb5974716871
# Parent  b52a12559d92e0b3cde437f50373242d9f1a1b11
consolidate less aggressively: avoid live-lock when PIDE round-trip takes too long (e.g. in complex theory hierarchies);

diff -r b52a12559d92 -r f326596f5752 etc/options
--- a/etc/options	Tue Oct 01 19:08:24 2019 +0200
+++ b/etc/options	Tue Oct 01 19:54:42 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 = 2.0
+public option editor_consolidate_delay : real = 3.0
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 public option editor_prune_delay : real = 15
diff -r b52a12559d92 -r f326596f5752 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Oct 01 19:08:24 2019 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Oct 01 19:54:42 2019 +0200
@@ -399,7 +399,7 @@
     {
       require(prover.defined)
 
-      prover.get.discontinue_execution()
+      if (edits.nonEmpty) prover.get.discontinue_execution()
 
       val previous = global_state.value.history.tip.version
       val version = Future.promise[Document.Version]
diff -r b52a12559d92 -r f326596f5752 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue Oct 01 19:08:24 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Tue Oct 01 19:54:42 2019 +0200
@@ -126,6 +126,7 @@
           "ML_statistics=false" +
           "parallel_proofs=0" +
           "editor_tracing_messages=0" +
+          "editor_consolidate_delay=10" +
           "editor_presentation"
       (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
     }