# HG changeset patch
# User wenzelm
# Date 1662235251 -7200
# Node ID d6c6e787cd86f36e6c31814f120de93c38f6de98
# Parent  92aa9ac31c7c7da90b1c899d224b8885bb161505
tuned signature;

diff -r 92aa9ac31c7c -r d6c6e787cd86 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Sep 03 21:27:33 2022 +0200
+++ b/src/Pure/PIDE/resources.ML	Sat Sep 03 22:00:51 2022 +0200
@@ -256,9 +256,11 @@
     SOME qualifier => qualifier
   | NONE => Long_Name.qualifier theory);
 
+fun literal_theory theory =
+  Long_Name.is_qualified theory orelse is_some (global_theory theory);
+
 fun theory_name qualifier theory =
-  if Long_Name.is_qualified theory orelse is_some (global_theory theory)
-  then theory
+  if literal_theory theory then theory
   else Long_Name.qualify qualifier theory;
 
 fun theory_bibtex_entries theory =
diff -r 92aa9ac31c7c -r d6c6e787cd86 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Sep 03 21:27:33 2022 +0200
+++ b/src/Pure/PIDE/resources.scala	Sat Sep 03 22:00:51 2022 +0200
@@ -150,8 +150,11 @@
   def global_theory(theory: String): Boolean =
     sessions_structure.global_theories.isDefinedAt(theory)
 
+  def literal_theory(theory: String): Boolean =
+    Long_Name.is_qualified(theory) || global_theory(theory)
+
   def theory_name(qualifier: String, theory: String): String =
-    if (Long_Name.is_qualified(theory) || global_theory(theory)) theory
+    if (literal_theory(theory)) theory
     else Long_Name.qualify(qualifier, theory)
 
   def find_theory_node(theory: String): Option[Document.Node.Name] = {
@@ -173,7 +176,7 @@
       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)
+          if (Thy_Header.is_base_name(s) && literal_theory(s)) loaded_theory_node(theory)
           else file_node(Path.explode(s).thy, dir = dir, theory = theory)
       }
     }