# HG changeset patch
# User wenzelm
# Date 1691947433 -7200
# Node ID 374611eb30550d3f9a0035eeaf0d5f38fcc60c53
# Parent  fd3fa1790a96fd17c11302caa71de44b6d8b2913
tuned signature: more operations for formal theory context vs. theory loader;

diff -r fd3fa1790a96 -r 374611eb3055 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Aug 13 17:50:31 2023 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Aug 13 19:23:53 2023 +0200
@@ -17,6 +17,7 @@
   val lookup_theory: string -> theory option
   val defined_theory: string -> bool
   val get_theory: string -> theory
+  val check_theory: Proof.context -> string * Position.T -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
   val use_theories: Options.T -> string -> (string * Position.T) list ->
@@ -151,6 +152,8 @@
 
 val get_imports = Resources.imports_of o get_theory;
 
+val check_theory = Theory.check_theory {get = get_theory, all = get_names};
+
 
 
 (** thy operations **)
diff -r fd3fa1790a96 -r 374611eb3055 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Aug 13 17:50:31 2023 +0200
+++ b/src/Pure/theory.ML	Sun Aug 13 19:23:53 2023 +0200
@@ -15,6 +15,8 @@
   val get_pure: unit -> theory
   val get_pure_bootstrap: unit -> theory
   val get_markup: theory -> Markup.T
+  val check_theory: {get: string -> theory, all: unit -> string list} ->
+    Proof.context -> string * Position.T -> theory
   val check: {long: bool} -> Proof.context -> string * Position.T -> theory
   val axiom_table: theory -> term Name_Space.table
   val axiom_space: theory -> Name_Space.T
@@ -137,23 +139,27 @@
   let val {pos, id, ...} = rep_theory thy
   in theory_markup {def = false} (Context.theory_long_name thy) id pos end;
 
-fun check long ctxt (name, pos) =
+fun check_theory {get, all} ctxt (name, pos) =
+  let
+    val thy = get name handle ERROR msg =>
+      let
+        val completion_report =
+          Completion.make_report (name, pos)
+            (fn completed =>
+              all ()
+              |> filter (completed o Long_Name.base_name)
+              |> sort_strings
+              |> map (fn a => (a, (Markup.theoryN, a))));
+      in error (msg ^ Position.here pos ^ completion_report) end;
+    val _ = Context_Position.report ctxt pos (get_markup thy);
+  in thy end;
+
+fun check long ctxt arg =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val thy' =
-      Context.get_theory long thy name
-        handle ERROR msg =>
-          let
-            val completion_report =
-              Completion.make_report (name, pos)
-                (fn completed =>
-                  map (Context.theory_name long) (ancestors_of thy)
-                  |> filter (completed o Long_Name.base_name)
-                  |> sort_strings
-                  |> map (fn a => (a, (Markup.theoryN, a))));
-          in error (msg ^ Position.here pos ^ completion_report) end;
-    val _ = Context_Position.report ctxt pos (get_markup thy');
-  in thy' end;
+    val get = Context.get_theory long thy;
+    fun all () = map (Context.theory_name long) (ancestors_of thy);
+  in check_theory {get = get, all = all} ctxt arg end;
 
 
 (* basic operations *)