# HG changeset patch
# User wenzelm
# Date 1662236722 -7200
# Node ID f1dc3d9d5164e154ee3ca32c8b1db0f9f06a38a0
# Parent  d6c6e787cd86f36e6c31814f120de93c38f6de98
check imports more strictly, e.g. reject ".../Pure" or ".../HOL-Library.Multiset";

diff -r d6c6e787cd86 -r f1dc3d9d5164 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Sep 03 22:00:51 2022 +0200
+++ b/src/Pure/PIDE/resources.ML	Sat Sep 03 22:25:22 2022 +0200
@@ -287,6 +287,11 @@
   let
     val theory = theory_name qualifier (Thy_Header.import_name s);
     fun theory_node path = make_theory_node path theory;
+    val literal_import = literal_theory theory andalso qualifier <> theory_qualifier theory;
+    val _ =
+      if literal_import andalso not (Thy_Header.is_base_name s) then
+        error ("Bad import of theory from other session via file-path: " ^ quote s)
+      else ();
   in
     if loaded_theory theory then loaded_theory_node theory
     else
diff -r d6c6e787cd86 -r f1dc3d9d5164 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Sep 03 22:00:51 2022 +0200
+++ b/src/Pure/PIDE/resources.scala	Sat Sep 03 22:25:22 2022 +0200
@@ -171,6 +171,11 @@
 
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = {
     val theory = theory_name(qualifier, Thy_Header.import_name(s))
+    val literal_import =
+      literal_theory(theory) && qualifier != sessions_structure.theory_qualifier(theory)
+    if (literal_import && !Thy_Header.is_base_name(s)) {
+      error("Bad import of theory from other session via file-path: " + quote(s))
+    }
     if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
     else {
       find_theory_node(theory) match {