tuned signature;
authorwenzelm
Mon Nov 06 17:24:09 2017 +0100 (18 months ago)
changeset 670151a9e2a2bf251
parent 67014 e6a695d6a6b2
child 67016 57d58c3cf16b
tuned signature;
src/Pure/PIDE/resources.scala
src/Tools/VSCode/src/vscode_resources.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Mon Nov 06 16:03:13 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Nov 06 17:24:09 2017 +0100
     1.3 @@ -19,8 +19,25 @@
     1.4  {
     1.5    resources =>
     1.6  
     1.7 +
     1.8 +  /* theory files */
     1.9 +
    1.10    def thy_path(path: Path): Path = path.ext("thy")
    1.11  
    1.12 +  def thy_node_name(qualifier: String, file: JFile, bootstrap: Boolean = false)
    1.13 +    : Document.Node.Name =
    1.14 +  {
    1.15 +    session_base.known.get_file(file, bootstrap) getOrElse {
    1.16 +      val node = file.getPath
    1.17 +      theory_name(qualifier, Thy_Header.theory_name(node)) match {
    1.18 +        case (true, theory) => Document.Node.Name.loaded_theory(theory)
    1.19 +        case (false, theory) =>
    1.20 +          val master_dir = if (theory == "") "" else file.getParent
    1.21 +          Document.Node.Name(node, master_dir, theory)
    1.22 +      }
    1.23 +    }
    1.24 +  }
    1.25 +
    1.26  
    1.27    /* file-system operations */
    1.28  
     2.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Nov 06 16:03:13 2017 +0100
     2.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Nov 06 17:24:09 2017 +0100
     2.3 @@ -91,15 +91,7 @@
     2.4    def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
     2.5  
     2.6    def node_name(file: JFile): Document.Node.Name =
     2.7 -    session_base.known.get_file(file, bootstrap = true) getOrElse {
     2.8 -      val node = file.getPath
     2.9 -      theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
    2.10 -        case (true, theory) => Document.Node.Name.loaded_theory(theory)
    2.11 -        case (false, theory) =>
    2.12 -          val master_dir = if (theory == "") "" else file.getParent
    2.13 -          Document.Node.Name(node, master_dir, theory)
    2.14 -      }
    2.15 -    }
    2.16 +    thy_node_name(Sessions.DRAFT, file, bootstrap = true)
    2.17  
    2.18    override def append(dir: String, source_path: Path): String =
    2.19    {