--- 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)