28213
|
1 |
theory Setup
|
28419
|
2 |
imports Complex_Main
|
28213
|
3 |
uses "../../../antiquote_setup.ML"
|
|
4 |
begin
|
|
5 |
|
28419
|
6 |
ML {* no_document use_thys ["Efficient_Nat", "Code_Char_chr"] *}
|
|
7 |
|
28213
|
8 |
ML_val {* Code_Target.code_width := 74 *}
|
|
9 |
|
28419
|
10 |
ML {*
|
|
11 |
fun pr_class ctxt = Sign.extern_class (ProofContext.theory_of ctxt)
|
|
12 |
o Sign.read_class (ProofContext.theory_of ctxt);
|
|
13 |
*}
|
|
14 |
|
|
15 |
ML {*
|
|
16 |
val _ = ThyOutput.add_commands
|
|
17 |
[("class", ThyOutput.args (Scan.lift Args.name) (K pr_class))]
|
|
18 |
*}
|
|
19 |
|
|
20 |
ML {*
|
|
21 |
val verbatim_line = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
|
|
22 |
val verbatim_lines = rev
|
|
23 |
#> dropwhile (fn s => s = "")
|
|
24 |
#> rev
|
|
25 |
#> map verbatim_line #> space_implode "\\newline%\n"
|
|
26 |
#> prefix "\\isaverbatim%\n\\noindent%\n"
|
|
27 |
*}
|
|
28 |
|
|
29 |
ML {*
|
|
30 |
local
|
|
31 |
|
|
32 |
val parse_const_terms = Scan.repeat1 Args.term
|
|
33 |
>> (fn ts => fn thy => map (Code_Unit.check_const thy) ts);
|
|
34 |
val parse_consts = Scan.lift (Args.parens (Args.$$$ "consts")) |-- parse_const_terms
|
|
35 |
>> (fn mk_cs => fn thy => map (Code_Name.const thy) (mk_cs thy));
|
|
36 |
val parse_types = Scan.lift (Args.parens (Args.$$$ "types") |-- Scan.repeat1 Args.name)
|
|
37 |
>> (fn tycos => fn thy => map (Code_Name.tyco thy o Sign.intern_type thy) tycos);
|
|
38 |
val parse_classes = Scan.lift (Args.parens (Args.$$$ "classes") |-- Scan.repeat1 Args.name)
|
|
39 |
>> (fn classes => fn thy => map (Code_Name.class thy o Sign.intern_class thy) classes);
|
|
40 |
val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name))
|
|
41 |
>> (fn insts => fn thy => map (Code_Name.instance thy o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts);
|
|
42 |
val parse_names = parse_consts || parse_types || parse_classes || parse_instances;
|
|
43 |
|
|
44 |
fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) =
|
|
45 |
Code_Target.code_of (ProofContext.theory_of ctxt)
|
|
46 |
target "Example" (mk_cs (ProofContext.theory_of ctxt))
|
|
47 |
(maps (fn f => f (ProofContext.theory_of ctxt)) mk_stmtss)
|
|
48 |
|> split_lines
|
|
49 |
|> verbatim_lines;
|
|
50 |
|
|
51 |
in
|
|
52 |
|
|
53 |
val _ = ThyOutput.add_commands
|
|
54 |
[("code_stmts", ThyOutput.args
|
|
55 |
(parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
|
|
56 |
code_stmts)]
|
|
57 |
|
28213
|
58 |
end
|
28419
|
59 |
*}
|
|
60 |
|
|
61 |
end
|