src/Tools/jEdit/src/document_model.scala

--- a/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 13:28:37 2016 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 15:31:13 2016 +0100
@@ -73,25 +73,13 @@
 
   def is_theory: Boolean = node_name.is_theory
 
-  def is_ml_root: Boolean =
-    Thy_Header.ml_roots.exists({ case (_, name) => name == node_name.theory })
-
-  def is_bootstrap_thy: Boolean =
-    Thy_Header.bootstrap_thys.exists({ case (_, name) => name == node_name.theory })
-
   def node_header(): Document.Node.Header =
   {
     GUI_Thread.require {}
 
-    if (is_ml_root)
-      Document.Node.Header(
-        List((PIDE.resources.import_name("", node_name, Thy_Header.ML_BOOTSTRAP), Position.none)))
-    else if (is_theory) {
-      if (is_bootstrap_thy) {
-        Document.Node.Header(
-          List((PIDE.resources.import_name("", node_name, Thy_Header.PURE), Position.none)))
-      }
-      else {
+    PIDE.resources.special_header(node_name) getOrElse
+    {
+      if (is_theory) {
         JEdit_Lib.buffer_lock(buffer) {
           Token_Markup.line_token_iterator(
             Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
@@ -103,12 +91,13 @@
                 val length = buffer.getLength - offset
                 PIDE.resources.check_thy_reader("", node_name,
                   new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command)
-              case None => Document.Node.no_header
+              case None =>
+                Document.Node.no_header
             }
         }
       }
+      else Document.Node.no_header
     }
-    else Document.Node.no_header
   }