# HG changeset patch
# User wenzelm
# Date 1509985449 -3600
# Node ID 1a9e2a2bf251a5eb2d1c84222fb099af1be79db7
# Parent  e6a695d6a6b24d9e3e7c81a86badcd2e1524e129
tuned signature;

diff -r e6a695d6a6b2 -r 1a9e2a2bf251 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Nov 06 16:03:13 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Mon Nov 06 17:24:09 2017 +0100
@@ -19,8 +19,25 @@
 {
   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 */
 
diff -r e6a695d6a6b2 -r 1a9e2a2bf251 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Nov 06 16:03:13 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Nov 06 17:24:09 2017 +0100
@@ -91,15 +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, 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)
-      }
-    }
+    thy_node_name(Sessions.DRAFT, file, bootstrap = true)
 
   override def append(dir: String, source_path: Path): String =
   {