src/Doc/more_antiquote.ML
author haftmann
Mon Feb 06 20:56:34 2017 +0100 (2017-02-06)
changeset 64990 c6a7de505796
parent 63554 d7c6a3a01b79
child 67386 998e01d6f8fd
permissions -rw-r--r--
more explicit errors in pathological cases
     1 (*  Title:      Doc/more_antiquote.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 More antiquotations (partly depending on Isabelle/HOL).
     5 *)
     6 
     7 structure More_Antiquote : sig end =
     8 struct
     9 
    10 (* class specifications *)
    11 
    12 local
    13 
    14 fun class_spec ctxt s =
    15   let
    16     val thy = Proof_Context.theory_of ctxt;
    17     val class = Sign.intern_class thy s;
    18   in Thy_Output.output ctxt (Class.pretty_specification thy class) end;
    19 
    20 in
    21 
    22 val _ =
    23   Theory.setup (Thy_Output.antiquotation @{binding class_spec} (Scan.lift Args.name)
    24     (fn {context, ...} => class_spec context));
    25 
    26 end;
    27 
    28 
    29 (* code theorem antiquotation *)
    30 
    31 local
    32 
    33 fun no_vars ctxt thm =
    34   let
    35     val ctxt' = Variable.set_body false ctxt;
    36     val ((_, [thm]), _) = Variable.import true [thm] ctxt';
    37   in thm end;
    38 
    39 fun pretty_code_thm ctxt raw_const =
    40   let
    41     val thy = Proof_Context.theory_of ctxt;
    42     val const = Code.check_const thy raw_const;
    43     val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
    44     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    45     val thms = Code_Preproc.cert eqngr const
    46       |> Code.equations_of_cert thy
    47       |> snd
    48       |> these
    49       |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
    50       |> map (holize o no_vars ctxt o Axclass.overload ctxt);
    51   in Thy_Output.output ctxt (map (Thy_Output.pretty_thm ctxt) thms) end;
    52 
    53 in
    54 
    55 val _ =
    56   Theory.setup (Thy_Output.antiquotation @{binding code_thms} Args.term
    57     (fn {context, ...} => pretty_code_thm context));
    58 
    59 end;
    60 
    61 end;