# HG changeset patch
# User wenzelm
# Date 1667383282 -3600
# Node ID aaf307f865c94e4196f5bad11737c38c4f132458
# Parent  4de3d831ff4d00fb05913d05dcc92ecac6c1a369
tuned signature;

diff -r 4de3d831ff4d -r aaf307f865c9 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Nov 02 10:24:44 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Wed Nov 02 11:01:22 2022 +0100
@@ -534,7 +534,7 @@
         |> map_filter (Command.exec_parallel_prints execution_id [delay]);
 
       fun finished_import (name, (node, _)) =
-        finished_result node orelse is_some (Thy_Info.lookup_theory name);
+        finished_result node orelse Thy_Info.defined_theory name;
 
       val nodes = nodes_of (the_version state version_id);
       val required = make_required nodes;
@@ -642,7 +642,7 @@
   in parent |> Option.map (fn thy => Resources.begin_theory master_dir header [thy]) end;
 
 fun check_theory full name node =
-  is_some (Thy_Info.lookup_theory name) orelse
+  Thy_Info.defined_theory name orelse
   null (#errors (get_header node)) andalso (not full orelse is_some (get_result node));
 
 fun last_common keywords state node_required node0 node =
diff -r 4de3d831ff4d -r aaf307f865c9 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Nov 02 10:24:44 2022 +0100
+++ b/src/Pure/Thy/thy_info.ML	Wed Nov 02 11:01:22 2022 +0100
@@ -15,6 +15,7 @@
   val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory
   val get_names: unit -> string list
   val lookup_theory: string -> theory option
+  val defined_theory: string -> bool
   val get_theory: string -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
@@ -138,6 +139,8 @@
     SOME (_, SOME theory) => SOME theory
   | _ => NONE);
 
+val defined_theory = is_some o lookup_theory;
+
 fun get_theory name =
   (case lookup_theory name of
     SOME theory => theory