clarified: consolidated result is last command;
authorwenzelm
Thu, 31 May 2018 22:10:06 +0200
changeset 68335 2f080a51a10d
parent 68334 ed40728c45d0
child 68336 09ac56914b29
clarified: consolidated result is last command;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.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 =
     {
--- 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)