--- a/src/Pure/PIDE/command.scala Tue May 29 20:03:24 2018 +0200
+++ b/src/Pure/PIDE/command.scala Tue May 29 22:25:59 2018 +0200
@@ -260,6 +260,8 @@
exports: Exports = Exports.empty,
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)
@@ -565,6 +567,8 @@
val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
+ def potentially_initialized: Boolean = span.name == Thy_Header.THEORY
+
/* blobs */