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