# HG changeset patch
# User wenzelm
# Date 1568227690 -7200
# Node ID 4c53227f4b73548d84e7a76eebc8935d70df01e2
# Parent  a6c0f2d106c857b12869b84ffc6e36621425256f
find theory node name via session directories;

diff -r a6c0f2d106c8 -r 4c53227f4b73 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Sep 11 16:06:10 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Sep 11 20:48:10 2019 +0200
@@ -135,7 +135,7 @@
   def import_name(info: Sessions.Info, s: String): Document.Node.Name =
     import_name(info.name, info.dir.implode, s)
 
-  def theory_name(default_qualifier: String, file: JFile): Option[Document.Node.Name] =
+  def find_theory(default_qualifier: String, file: JFile): Option[Document.Node.Name] =
   {
     val dir = File.canonical(file).getParentFile
     val qualifier = session_base.session_directories.get(dir).getOrElse(default_qualifier)
diff -r a6c0f2d106c8 -r 4c53227f4b73 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Sep 11 16:06:10 2019 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Sep 11 20:48:10 2019 +0200
@@ -94,7 +94,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 {
+    find_theory(Sessions.DRAFT, file) getOrElse {
       val node = file.getPath
       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
       if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
diff -r a6c0f2d106c8 -r 4c53227f4b73 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Sep 11 16:06:10 2019 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Sep 11 20:48:10 2019 +0200
@@ -36,11 +36,8 @@
 
   /* document node name */
 
-  def known_file(path: String): Option[Document.Node.Name] =
-    JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_, bootstrap = true))
-
   def node_name(path: String): Document.Node.Name =
-    known_file(path) getOrElse {
+    JEdit_Lib.check_file(path).flatMap(file => find_theory(Sessions.DRAFT, file)) getOrElse {
       val vfs = VFSManager.getVFSForPath(path)
       val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))