| changeset 68381 | 2fd3a6d6ba2e |
| parent 68335 | 2f080a51a10d |
| child 68728 | c07f6fa02c59 |
--- a/src/Pure/PIDE/command.scala Tue Jun 05 14:15:49 2018 +0200 +++ b/src/Pure/PIDE/command.scala Tue Jun 05 16:12:26 2018 +0200 @@ -263,6 +263,8 @@ def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED) def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED) + lazy val maybe_consolidated: Boolean = Protocol.maybe_consolidated(status) + lazy val protocol_status: Protocol.Status = { val warnings =