# HG changeset patch
# User wenzelm
# Date 1482762673 -3600
# Node ID b5965890e54dc49c2010b6c91a12526fffbaa3d5
# Parent  d8e0619abb60494eded4f935eeb6d9e168b17c69
more uniform treatment of file name vs. theory name and special header;

diff -r d8e0619abb60 -r b5965890e54d src/Pure/PIDE/resources.scala
--- 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(
diff -r d8e0619abb60 -r b5965890e54d src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Dec 26 13:28:37 2016 +0100
+++ b/src/Pure/Thy/thy_header.scala	Mon Dec 26 15:31:13 2016 +0100
@@ -69,7 +69,7 @@
     Outer_Syntax.init().add_keywords(bootstrap_header)
 
 
-  /* file name */
+  /* file name vs. theory name */
 
   val PURE = "Pure"
   val ML_BOOTSTRAP = "ML_Bootstrap"
@@ -94,6 +94,12 @@
       case _ => None
     }
 
+  def is_ml_root(theory: String): Boolean =
+    ml_roots.exists({ case (_, b) => b == theory })
+
+  def is_bootstrap(theory: String): Boolean =
+    bootstrap_thys.exists({ case (_, b) => b == theory })
+
 
   /* header */
 
diff -r d8e0619abb60 -r b5965890e54d src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Mon Dec 26 13:28:37 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Mon Dec 26 15:31:13 2016 +0100
@@ -20,11 +20,14 @@
 
   def is_theory: Boolean = node_name.is_theory
 
-  lazy val node_header: Document.Node.Header =
-    if (is_theory)
-      session.resources.check_thy_reader(
-        "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command)
-    else Document.Node.no_header
+  def node_header(resources: VSCode_Resources): Document.Node.Header =
+    resources.special_header(node_name) getOrElse
+    {
+      if (is_theory)
+        session.resources.check_thy_reader(
+          "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command)
+      else Document.Node.no_header
+    }
 
 
   /* edits */
@@ -32,9 +35,9 @@
   def text_edits: List[Text.Edit] =
     if (changed) List(Text.Edit.insert(0, doc.make_text)) else Nil
 
-  def node_edits: List[Document.Edit_Text] =
+  def node_edits(resources: VSCode_Resources): List[Document.Edit_Text] =
     if (changed) {
-      List(session.header_edit(node_name, node_header),
+      List(session.header_edit(node_name, node_header(resources)),
         node_name -> Document.Node.Clear(),
         node_name -> Document.Node.Edits(text_edits),
         node_name ->
diff -r d8e0619abb60 -r b5965890e54d src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Mon Dec 26 13:28:37 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Mon Dec 26 15:31:13 2016 +0100
@@ -200,7 +200,7 @@
         {
           val models = st.models
           val changed = (for { entry <- models.iterator if entry._2.changed } yield entry).toList
-          val edits = for { (_, model) <- changed; edit <- model.node_edits } yield edit
+          val edits = for { (_, model) <- changed; edit <- model.node_edits(resources) } yield edit
           val models1 =
             (models /: changed)({ case (m, (uri, model)) => m + (uri -> model.unchanged) })
 
diff -r d8e0619abb60 -r b5965890e54d 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
   }