src/Pure/PIDE/command.scala
changeset 68323 bf7336731981
parent 68306 d575281e18d0
child 68335 2f080a51a10d
--- 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 */