--- a/src/Pure/PIDE/resources.scala Sun Nov 12 19:46:19 2017 +0100
+++ b/src/Pure/PIDE/resources.scala Sun Nov 12 19:47:18 2017 +0100
@@ -19,25 +19,8 @@
{
resources =>
-
- /* theory files */
-
def thy_path(path: Path): Path = path.ext("thy")
- def thy_node_name(qualifier: String, file: JFile, bootstrap: Boolean = false)
- : Document.Node.Name =
- {
- session_base.known.get_file(file, bootstrap) getOrElse {
- val node = file.getPath
- theory_name(qualifier, Thy_Header.theory_name(node)) match {
- case (true, theory) => Document.Node.Name.loaded_theory(theory)
- case (false, theory) =>
- val master_dir = if (theory == "") "" else file.getParent
- Document.Node.Name(node, master_dir, theory)
- }
- }
- }
-
/* file-system operations */
--- a/src/Tools/VSCode/src/vscode_resources.scala Sun Nov 12 19:46:19 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Sun Nov 12 19:47:18 2017 +0100
@@ -91,7 +91,15 @@
def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
def node_name(file: JFile): Document.Node.Name =
- thy_node_name(Sessions.DRAFT, file, bootstrap = true)
+ 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)
+ case (false, theory) =>
+ val master_dir = if (theory == "") "" else file.getParent
+ Document.Node.Name(node, master_dir, theory)
+ }
+ }
override def append(dir: String, source_path: Path): String =
{