--- a/src/Doc/more_antiquote.ML Thu Jan 18 21:29:28 2018 +0100
+++ b/src/Doc/more_antiquote.ML Thu Jan 18 21:41:30 2018 +0100
@@ -9,53 +9,37 @@
(* class specifications *)
-local
-
-fun class_spec ctxt s =
- let
- val thy = Proof_Context.theory_of ctxt;
- val class = Sign.intern_class thy s;
- in Thy_Output.output ctxt (Class.pretty_specification thy class) end;
-
-in
-
val _ =
- Theory.setup (Document_Antiquotation.setup @{binding class_spec} (Scan.lift Args.name)
- (fn {context, ...} => class_spec context));
-
-end;
+ Theory.setup (Thy_Output.antiquotation @{binding class_spec} (Scan.lift Args.name)
+ (fn ctxt => fn s =>
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val class = Sign.intern_class thy s;
+ in Class.pretty_specification thy class end));
(* code theorem antiquotation *)
-local
-
fun no_vars ctxt thm =
let
val ctxt' = Variable.set_body false ctxt;
val ((_, [thm]), _) = Variable.import true [thm] ctxt';
in thm end;
-fun pretty_code_thm ctxt raw_const =
- let
- val thy = Proof_Context.theory_of ctxt;
- val const = Code.check_const thy raw_const;
- val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
- fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
- val thms = Code_Preproc.cert eqngr const
- |> Code.equations_of_cert thy
- |> snd
- |> these
- |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
- |> map (holize o no_vars ctxt o Axclass.overload ctxt);
- in Thy_Output.output ctxt (map (Thy_Output.pretty_thm ctxt) thms) end;
-
-in
-
val _ =
- Theory.setup (Document_Antiquotation.setup @{binding code_thms} Args.term
- (fn {context, ...} => pretty_code_thm context));
+ Theory.setup (Thy_Output.antiquotation_pretty @{binding code_thms} Args.term
+ (fn ctxt => fn raw_const =>
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val const = Code.check_const thy raw_const;
+ val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
+ fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
+ val thms = Code_Preproc.cert eqngr const
+ |> Code.equations_of_cert thy
+ |> snd
+ |> these
+ |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
+ |> map (holize o no_vars ctxt o Axclass.overload ctxt);
+ in map (Thy_Output.pretty_thm ctxt) thms end));
end;
-
-end;