src/Pure/PIDE/command.scala
changeset 68324 bf7336731981
parent 68307 d575281e18d0
child 68336 2f080a51a10d
     1.1 --- a/src/Pure/PIDE/command.scala	Tue May 29 20:03:24 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue May 29 22:25:59 2018 +0200
     1.3 @@ -260,6 +260,8 @@
     1.4      exports: Exports = Exports.empty,
     1.5      markups: Markups = Markups.empty)
     1.6    {
     1.7 +    def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
     1.8 +
     1.9      lazy val consolidated: Boolean =
    1.10        status.exists(markup => markup.name == Markup.CONSOLIDATED)
    1.11  
    1.12 @@ -565,6 +567,8 @@
    1.13    val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
    1.14    val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
    1.15  
    1.16 +  def potentially_initialized: Boolean = span.name == Thy_Header.THEORY
    1.17 +
    1.18  
    1.19    /* blobs */
    1.20