--- a/src/Pure/theory.ML Thu Apr 16 15:55:55 2015 +0200
+++ b/src/Pure/theory.ML Thu Apr 16 20:54:01 2015 +0200
@@ -16,6 +16,7 @@
val setup: (theory -> theory) -> unit
val local_setup: (Proof.context -> Proof.context) -> unit
val get_markup: theory -> Markup.T
+ val check: Proof.context -> string * Position.T -> theory
val axiom_table: theory -> term Name_Space.table
val axiom_space: theory -> Name_Space.T
val axioms_of: theory -> (string * term) list
@@ -128,6 +129,25 @@
let val {pos, id, ...} = rep_theory thy
in theory_markup false (Context.theory_name thy) id pos end;
+fun check ctxt (name, pos) =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val thy' =
+ Context.get_theory thy name
+ handle ERROR msg =>
+ let
+ val completion =
+ Completion.make (name, pos)
+ (fn completed =>
+ map Context.theory_name (ancestors_of thy)
+ |> filter completed
+ |> sort_strings
+ |> map (fn a => (a, (Markup.theoryN, a))));
+ val report = Markup.markup_report (Completion.reported_text completion);
+ in error (msg ^ Position.here pos ^ report) end;
+ val _ = Context_Position.report ctxt pos (get_markup thy');
+ in thy' end;
+
(* basic operations *)