# HG changeset patch
# User wenzelm
# Date 1568668845 -7200
# Node ID 5bb025e24224180d43b764132d49aa6ad54250c8
# Parent  cceb10dcc9f9223c90528e9cac04a0a389d35412
clarified inversion of file name to theory name, notably for Windows;

diff -r cceb10dcc9f9 -r 5bb025e24224 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Sep 16 21:42:22 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Sep 16 23:20:45 2019 +0200
@@ -154,14 +154,15 @@
   def import_name(info: Sessions.Info, s: String): Document.Node.Name =
     import_name(info.name, info.dir.implode, s)
 
-  def find_theory(default_qualifier: String, file: JFile): Option[Document.Node.Name] =
+  def find_theory(file: JFile): Option[Document.Node.Name] =
   {
-    val dir = File.canonical(file).getParentFile
-    val qualifier = session_base.session_directories.get(dir).getOrElse(default_qualifier)
-    Thy_Header.theory_name(file.getName) match {
-      case "" => None
-      case s => Some(import_name(qualifier, File.path(file).dir.implode, s))
-    }
+    for {
+      qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile)
+      theory_base <- proper_string(Thy_Header.theory_name(file.getName))
+      theory = theory_name(qualifier, theory_base)
+      theory_node <- find_theory_node(theory)
+      if File.eq(theory_node.path.file, file)
+    } yield theory_node
   }
 
   def dump_checkpoints(info: Sessions.Info): Set[Document.Node.Name] =
diff -r cceb10dcc9f9 -r 5bb025e24224 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Sep 16 21:42:22 2019 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Sep 16 23:20:45 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 =
-    find_theory(Sessions.DRAFT, file) getOrElse {
+    find_theory(file) getOrElse {
       val node = file.getPath
       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
       if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
diff -r cceb10dcc9f9 -r 5bb025e24224 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Sep 16 21:42:22 2019 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Sep 16 23:20:45 2019 +0200
@@ -37,7 +37,7 @@
   /* document node name */
 
   def node_name(path: String): Document.Node.Name =
-    JEdit_Lib.check_file(path).flatMap(file => find_theory(Sessions.DRAFT, file)) getOrElse {
+    JEdit_Lib.check_file(path).flatMap(find_theory(_)) 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))