--- a/src/Pure/PIDE/resources.scala Sat Sep 03 15:43:20 2022 +0200
+++ b/src/Pure/PIDE/resources.scala Sat Sep 03 17:20:35 2022 +0200
@@ -168,14 +168,13 @@
def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = {
val theory = theory_name(qualifier, Thy_Header.import_name(s))
- def theory_node = file_node(Path.explode(s).thy, dir = dir, theory = theory)
-
- if (!Thy_Header.is_base_name(s)) theory_node
- else if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
+ 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 (Long_Name.is_qualified(s)) loaded_theory_node(theory) else theory_node
+ case None =>
+ if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s)) loaded_theory_node(theory)
+ else file_node(Path.explode(s).thy, dir = dir, theory = theory)
}
}
}