src/Pure/PIDE/resources.scala
changeset 64673 b5965890e54d
parent 64657 6209e0f7a4e8
child 64718 3197b68f4314
     1.1 --- a/src/Pure/PIDE/resources.scala	Mon Dec 26 13:28:37 2016 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Dec 26 15:31:13 2016 +0100
     1.3 @@ -155,6 +155,16 @@
     1.4      catch { case ERROR(_) => false }
     1.5  
     1.6  
     1.7 +  /* special header */
     1.8 +
     1.9 +  def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
    1.10 +    if (Thy_Header.is_ml_root(name.theory))
    1.11 +      Some(Document.Node.Header(List((import_name("", name, Thy_Header.ML_BOOTSTRAP), Position.none))))
    1.12 +    else if (Thy_Header.is_bootstrap(name.theory))
    1.13 +      Some(Document.Node.Header(List((import_name("", name, Thy_Header.PURE), Position.none))))
    1.14 +    else None
    1.15 +
    1.16 +
    1.17    /* document changes */
    1.18  
    1.19    def parse_change(