--- 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 =
--- 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;
--- 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 ||
--- 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";
--- 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"