# HG changeset patch
# User wenzelm
# Date 1498485440 -7200
# Node ID bb886f13623a245325fd78da293bd4bce8786cec
# Parent  8d34d42c40cb7d85c39a127ec13aaa404462ea33
proper bootstrap_name (amending b42743f5b595);

diff -r 8d34d42c40cb -r bb886f13623a src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Jun 26 11:07:48 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Jun 26 15:57:20 2017 +0200
@@ -123,6 +123,7 @@
       override def toString: String = if (is_theory) theory else node
 
       def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
+      def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
     }
 
 
diff -r 8d34d42c40cb -r bb886f13623a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Jun 26 11:07:48 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Jun 26 15:57:20 2017 +0200
@@ -81,8 +81,11 @@
         theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
         files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
 
-    def get_file(file: JFile): Option[Document.Node.Name] =
-      files.getOrElse(file.getCanonicalFile, Nil).headOption
+    def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
+    {
+      val res = files.getOrElse(file.getCanonicalFile, Nil).headOption
+      if (bootstrap) res.map(_.map_theory(Thy_Header.bootstrap_name(_))) else res
+    }
   }
 
   object Base
diff -r 8d34d42c40cb -r bb886f13623a src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Jun 26 11:07:48 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala	Mon Jun 26 15:57:20 2017 +0200
@@ -89,8 +89,7 @@
 
   def theory_name(s: String): String =
     s match {
-      case Thy_File_Name(name) =>
-        bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name)
+      case Thy_File_Name(name) => bootstrap_name(name)
       case Import_Name(name) =>
         ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
       case _ => ""
@@ -102,6 +101,9 @@
   def is_bootstrap(theory: String): Boolean =
     bootstrap_thys.exists({ case (_, b) => b == theory })
 
+  def bootstrap_name(theory: String): String =
+    bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
+
 
   /* header */
 
diff -r 8d34d42c40cb -r bb886f13623a src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Jun 26 11:07:48 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Jun 26 15:57:20 2017 +0200
@@ -91,7 +91,7 @@
   def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
 
   def node_name(file: JFile): Document.Node.Name =
-    session_base.known.get_file(file) getOrElse {
+    session_base.known.get_file(file, bootstrap = true) getOrElse {
       val node = file.getPath
       theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
         case (true, theory) => Document.Node.Name.loaded_theory(theory)
diff -r 8d34d42c40cb -r bb886f13623a src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Jun 26 11:07:48 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Jun 26 15:57:20 2017 +0200
@@ -26,7 +26,7 @@
   /* document node name */
 
   def known_file(path: String): Option[Document.Node.Name] =
-    JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_))
+    JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_, bootstrap = true))
 
   def node_name(path: String): Document.Node.Name =
     known_file(path) getOrElse {