# HG changeset patch
# User wenzelm
# Date 1570020337 -7200
# Node ID 03474245359460811b3f1715122168005279a42d
# Parent  97b168f0c3a3fea639214d6f1d9177b06f231e8b
more robust: avoid update/interrupt of long-running print_consolidation;

diff -r 97b168f0c3a3 -r 034742453594 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Oct 01 20:21:30 2019 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Oct 02 14:45:37 2019 +0200
@@ -262,6 +262,7 @@
     markups: Markups = Markups.empty)
   {
     def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
+    def consolidating: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATING)
     def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
 
     lazy val maybe_consolidated: Boolean =
diff -r 97b168f0c3a3 -r 034742453594 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Oct 01 20:21:30 2019 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Oct 02 14:45:37 2019 +0200
@@ -748,9 +748,11 @@
                     segments = segments};
                 in
                   fn _ =>
-                    Exn.release
-                      (Exn.capture (Thy_Info.apply_presentation presentation_context) thy
-                        before commit_consolidated node)
+                    let
+                      val _ = Output.status [Markup.markup_only Markup.consolidating];
+                      val res = Exn.capture (Thy_Info.apply_presentation presentation_context) thy;
+                      val _ = commit_consolidated node;
+                    in Exn.release res end
                 end
               else fn _ => commit_consolidated node;
 
diff -r 97b168f0c3a3 -r 034742453594 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Oct 01 20:21:30 2019 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Oct 02 14:45:37 2019 +0200
@@ -897,16 +897,18 @@
       } yield (id -> command)).toMap
     }
 
-    def command_state_eval(version: Version, command: Command): Option[Command.State] =
+    def command_maybe_consolidated(version: Version, command: Command): Boolean =
     {
       require(is_assigned(version))
       try {
         the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match {
-          case eval_id :: _ => Some(the_dynamic_state(eval_id))
-          case Nil => None
+          case eval_id :: print_ids =>
+            the_dynamic_state(eval_id).maybe_consolidated &&
+            !print_ids.exists(print_id => the_dynamic_state(print_id).consolidating)
+          case Nil => false
         }
       }
-      catch { case _: State.Fail => None }
+      catch { case _: State.Fail => false }
     }
 
     private def command_states_self(version: Version, command: Command)
@@ -992,13 +994,7 @@
 
     def node_maybe_consolidated(version: Version, name: Node.Name): Boolean =
       name.is_theory &&
-      {
-        version.nodes(name).commands.reverse.iterator.forall(command =>
-          command_state_eval(version, command) match {
-            case None => false
-            case Some(st) => st.maybe_consolidated
-          })
-      }
+      version.nodes(name).commands.reverse.iterator.forall(command_maybe_consolidated(version, _))
 
     def node_consolidated(version: Version, name: Node.Name): Boolean =
       !name.is_theory ||
diff -r 97b168f0c3a3 -r 034742453594 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Oct 01 20:21:30 2019 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Oct 02 14:45:37 2019 +0200
@@ -182,6 +182,7 @@
   val canceledN: string val canceled: T
   val initializedN: string val initialized: T
   val finalizedN: string val finalized: T
+  val consolidatingN: string val consolidating: T
   val consolidatedN: string val consolidated: T
   val exec_idN: string
   val initN: string
@@ -631,6 +632,7 @@
 val (canceledN, canceled) = markup_elem "canceled";
 val (initializedN, initialized) = markup_elem "initialized";
 val (finalizedN, finalized) = markup_elem "finalized";
+val (consolidatingN, consolidating) = markup_elem "consolidating";
 val (consolidatedN, consolidated) = markup_elem "consolidated";
 
 
diff -r 97b168f0c3a3 -r 034742453594 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Oct 01 20:21:30 2019 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Oct 02 14:45:37 2019 +0200
@@ -467,6 +467,7 @@
   val CANCELED = "canceled"
   val INITIALIZED = "initialized"
   val FINALIZED = "finalized"
+  val CONSOLIDATING = "consolidating"
   val CONSOLIDATED = "consolidated"