author | wenzelm |
Tue, 25 Jan 2011 20:06:32 +0100 | |
changeset 41629 | 5490dc4d999d |
parent 39540 | 49c319fff40c |
child 42361 | 23f352990944 |
permissions | -rw-r--r-- |
30394 | 1 |
(* Title: doc-src/more_antiquote.ML |
28440 | 2 |
Author: Florian Haftmann, TU Muenchen |
3 |
||
4 |
More antiquotations. |
|
5 |
*) |
|
6 |
||
7 |
signature MORE_ANTIQUOTE = |
|
8 |
sig |
|
9 |
end; |
|
10 |
||
11 |
structure More_Antiquote : MORE_ANTIQUOTE = |
|
12 |
struct |
|
13 |
||
29397 | 14 |
(* code theorem antiquotation *) |
15 |
||
16 |
local |
|
17 |
||
18 |
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; |
|
19 |
||
20 |
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; |
|
21 |
||
22 |
fun no_vars ctxt thm = |
|
23 |
let |
|
24 |
val ctxt' = Variable.set_body false ctxt; |
|
31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents:
31156
diff
changeset
|
25 |
val ((_, [thm]), _) = Variable.import true [thm] ctxt'; |
29397 | 26 |
in thm end; |
27 |
||
28 |
fun pretty_code_thm src ctxt raw_const = |
|
29 |
let |
|
30 |
val thy = ProofContext.theory_of ctxt; |
|
31156 | 31 |
val const = Code.check_const thy raw_const; |
39540 | 32 |
val (_, eqngr) = Code_Preproc.obtain true thy [const] []; |
29874 | 33 |
fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm]; |
34896
a22b09addd78
adjusted to changes in code equation administration
haftmann
parents:
34072
diff
changeset
|
34 |
val thms = Code_Preproc.cert eqngr const |
35246 | 35 |
|> Code.equations_of_cert thy |
34896
a22b09addd78
adjusted to changes in code equation administration
haftmann
parents:
34072
diff
changeset
|
36 |
|> snd |
35246 | 37 |
|> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) |
29874 | 38 |
|> map (holize o no_vars ctxt o AxClass.overload thy); |
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
37216
diff
changeset
|
39 |
in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end; |
29397 | 40 |
|
41 |
in |
|
42 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36745
diff
changeset
|
43 |
val _ = Thy_Output.antiquotation "code_thms" Args.term |
30394 | 44 |
(fn {source, context, ...} => pretty_code_thm source context); |
29397 | 45 |
|
46 |
end; |
|
47 |
||
28440 | 48 |
end; |