# HG changeset patch
# User wenzelm
# Date 1492458533 -7200
# Node ID b42743f5b5951ee7628c58b3700314de09954d07
# Parent  a6644e0e87286a192ee309a51c9d5a91cf615602
prefer formal name from session context, for proper qualified theory name;

diff -r a6644e0e8728 -r b42743f5b595 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 17 21:26:23 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 17 21:48:53 2017 +0200
@@ -61,15 +61,15 @@
   def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
 
   def node_name(file: JFile): Document.Node.Name =
-  {
-    val node = file.getPath
-    theory_name(default_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)
+    session_base.known_file(file) getOrElse {
+      val node = file.getPath
+      theory_name(default_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)
+      }
     }
-  }
 
   override def append(dir: String, source_path: Path): String =
   {
diff -r a6644e0e8728 -r b42743f5b595 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 17 21:26:23 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 17 21:48:53 2017 +0200
@@ -25,17 +25,20 @@
 {
   /* document node name */
 
+  def known_file(path: String): Option[Document.Node.Name] =
+    JEdit_Lib.check_file(path).flatMap(session_base.known_file(_))
+
   def node_name(path: String): Document.Node.Name =
-  {
-    val vfs = VFSManager.getVFSForPath(path)
-    val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
-    theory_name(default_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 vfs.getParentOfPath(path)
-        Document.Node.Name(node, master_dir, theory)
+    known_file(path) getOrElse {
+      val vfs = VFSManager.getVFSForPath(path)
+      val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
+      theory_name(default_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 vfs.getParentOfPath(path)
+          Document.Node.Name(node, master_dir, theory)
+      }
     }
-  }
 
   def node_name(buffer: Buffer): Document.Node.Name =
     node_name(JEdit_Lib.buffer_name(buffer))