# 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))