# HG changeset patch
# User wenzelm
# Date 1568662942 -7200
# Node ID cceb10dcc9f9223c90528e9cac04a0a389d35412
# Parent  a8afe8eb3529cfce4c3ac8cc50438450d2f312f8
clarified import_name: observe directory notation more strictly;

diff -r a8afe8eb3529 -r cceb10dcc9f9 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Mon Sep 16 21:30:30 2019 +0200
+++ b/src/Pure/PIDE/resources.ML	Mon Sep 16 21:42:22 2019 +0200
@@ -112,7 +112,6 @@
 val check_doc = check_name #docs "documentation" (fn name => fn _ => Markup.doc name);
 
 
-
 (* manage source files *)
 
 type files =
@@ -170,20 +169,24 @@
       in if File.is_file path then SOME path else NONE end)
   end;
 
+fun make_theory_node node_name theory =
+  {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory};
+
+fun loaded_theory_node theory =
+  {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory};
+
 fun import_name qualifier dir s =
-  let val theory = theory_name qualifier (Thy_Header.import_name s) in
-    if loaded_theory theory
-    then {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}
+  let
+    val theory = theory_name qualifier (Thy_Header.import_name s);
+    fun theory_node () =
+      make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory;
+  in
+    if not (Thy_Header.is_base_name s) then theory_node ()
+    else if loaded_theory theory then loaded_theory_node theory
     else
-      let
-        val node_name =
-          (case find_theory_file theory of
-            SOME node_name => node_name
-          | NONE =>
-              if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
-              then Path.explode s
-              else File.full_path dir (thy_path (Path.expand (Path.explode s))));
-      in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end
+      (case find_theory_file theory of
+        SOME node_name => make_theory_node node_name theory
+      | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ())
   end;
 
 fun check_file dir file = File.check_file (File.full_path dir file);
diff -r a8afe8eb3529 -r cceb10dcc9f9 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Sep 16 21:30:30 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Sep 16 21:42:22 2019 +0200
@@ -136,14 +136,14 @@
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
   {
     val theory = theory_name(qualifier, Thy_Header.import_name(s))
-    if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
+    def theory_node = make_theory_node(dir, thy_path(Path.explode(s)), theory)
+
+    if (!Thy_Header.is_base_name(s)) theory_node
+    else if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
     else {
       find_theory_node(theory) match {
         case Some(node_name) => node_name
-        case None =>
-          if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s))
-            loaded_theory_node(theory)
-          else make_theory_node(dir, thy_path(Path.explode(s)), theory)
+        case None => if (Long_Name.is_qualified(s)) loaded_theory_node(theory) else theory_node
       }
     }
   }