proper bootstrap_name (amending b42743f5b595);
authorwenzelm
Mon Jun 26 15:57:20 2017 +0200 (24 months ago)
changeset 66195bb886f13623a
parent 66194 8d34d42c40cb
child 66196 31c9b09cc1d4
proper bootstrap_name (amending b42743f5b595);
src/Pure/PIDE/document.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_header.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Jun 26 11:07:48 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Jun 26 15:57:20 2017 +0200
     1.3 @@ -123,6 +123,7 @@
     1.4        override def toString: String = if (is_theory) theory else node
     1.5  
     1.6        def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
     1.7 +      def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
     1.8      }
     1.9  
    1.10  
     2.1 --- a/src/Pure/Thy/sessions.scala	Mon Jun 26 11:07:48 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Mon Jun 26 15:57:20 2017 +0200
     2.3 @@ -81,8 +81,11 @@
     2.4          theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
     2.5          files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
     2.6  
     2.7 -    def get_file(file: JFile): Option[Document.Node.Name] =
     2.8 -      files.getOrElse(file.getCanonicalFile, Nil).headOption
     2.9 +    def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
    2.10 +    {
    2.11 +      val res = files.getOrElse(file.getCanonicalFile, Nil).headOption
    2.12 +      if (bootstrap) res.map(_.map_theory(Thy_Header.bootstrap_name(_))) else res
    2.13 +    }
    2.14    }
    2.15  
    2.16    object Base
     3.1 --- a/src/Pure/Thy/thy_header.scala	Mon Jun 26 11:07:48 2017 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Jun 26 15:57:20 2017 +0200
     3.3 @@ -89,8 +89,7 @@
     3.4  
     3.5    def theory_name(s: String): String =
     3.6      s match {
     3.7 -      case Thy_File_Name(name) =>
     3.8 -        bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name)
     3.9 +      case Thy_File_Name(name) => bootstrap_name(name)
    3.10        case Import_Name(name) =>
    3.11          ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
    3.12        case _ => ""
    3.13 @@ -102,6 +101,9 @@
    3.14    def is_bootstrap(theory: String): Boolean =
    3.15      bootstrap_thys.exists({ case (_, b) => b == theory })
    3.16  
    3.17 +  def bootstrap_name(theory: String): String =
    3.18 +    bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
    3.19 +
    3.20  
    3.21    /* header */
    3.22  
     4.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Jun 26 11:07:48 2017 +0200
     4.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Jun 26 15:57:20 2017 +0200
     4.3 @@ -91,7 +91,7 @@
     4.4    def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
     4.5  
     4.6    def node_name(file: JFile): Document.Node.Name =
     4.7 -    session_base.known.get_file(file) getOrElse {
     4.8 +    session_base.known.get_file(file, bootstrap = true) getOrElse {
     4.9        val node = file.getPath
    4.10        theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
    4.11          case (true, theory) => Document.Node.Name.loaded_theory(theory)
     5.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Jun 26 11:07:48 2017 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Jun 26 15:57:20 2017 +0200
     5.3 @@ -26,7 +26,7 @@
     5.4    /* document node name */
     5.5  
     5.6    def known_file(path: String): Option[Document.Node.Name] =
     5.7 -    JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_))
     5.8 +    JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_, bootstrap = true))
     5.9  
    5.10    def node_name(path: String): Document.Node.Name =
    5.11      known_file(path) getOrElse {