back to more traditional import_name (reverting cceb10dcc9f9), e.g. relevant for "isabelle jedit -l CTT src/CTT/ex/Elimination.thy" to produce proper error "Cannot update finished theory CTT.Elimination";
--- a/src/Pure/PIDE/resources.ML Sat Sep 03 15:43:20 2022 +0200
+++ b/src/Pure/PIDE/resources.ML Sat Sep 03 17:20:35 2022 +0200
@@ -284,15 +284,16 @@
fun import_name qualifier dir s =
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;
+ fun theory_node path = make_theory_node path theory;
in
- if not (Thy_Header.is_base_name s) then theory_node ()
- else if loaded_theory theory then loaded_theory_node theory
+ if loaded_theory theory then loaded_theory_node theory
else
(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 ())
+ SOME node_name => theory_node node_name
+ | NONE =>
+ if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
+ then loaded_theory_node theory
+ else theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))))
end;
fun check_file dir file = File.check_file (File.full_path dir file);
--- 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)
}
}
}