# HG changeset patch
# User wenzelm
# Date 1527797406 -7200
# Node ID 2f080a51a10d8f8ae0e0f66525b2f5ae375a4e1a
# Parent  ed40728c45d03f527d221c43de03eb2516319cf8
clarified: consolidated result is last command;

diff -r ed40728c45d0 -r 2f080a51a10d src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu May 31 22:04:15 2018 +0200
+++ b/src/Pure/PIDE/command.scala	Thu May 31 22:10:06 2018 +0200
@@ -261,9 +261,7 @@
     markups: Markups = Markups.empty)
   {
     def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
-
-    lazy val consolidated: Boolean =
-      status.exists(markup => markup.name == Markup.CONSOLIDATED)
+    def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
 
     lazy val protocol_status: Protocol.Status =
     {
diff -r ed40728c45d0 -r 2f080a51a10d src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu May 31 22:04:15 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Thu May 31 22:10:06 2018 +0200
@@ -930,8 +930,10 @@
 
     def node_consolidated(version: Version, name: Node.Name): Boolean =
       !name.is_theory ||
-        version.nodes(name).commands.reverse.iterator.
-          flatMap(command_states(version, _)).exists(_.consolidated)
+      {
+        val it = version.nodes(name).commands.reverse.iterator
+        it.hasNext && command_states(version, it.next).exists(_.consolidated)
+      }
 
     // persistent user-view
     def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)