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";
authorwenzelm
Sat, 03 Sep 2022 17:20:35 +0200
changeset 76046 507c65cc4332
parent 76045 4aeb5f019e53
child 76047 f244926013e5
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";
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
--- 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)
       }
     }
   }