author | haftmann |
Fri, 24 Oct 2008 10:41:13 +0200 | |
changeset 28679 | d7384e8e99b3 |
parent 28634 | 764ef122a164 |
child 28714 | 1992553cccfe |
permissions | -rw-r--r-- |
haftmann@28440 | 1 |
(* Title: Doc/more_antiquote.ML |
haftmann@28440 | 2 |
ID: $Id$ |
haftmann@28440 | 3 |
Author: Florian Haftmann, TU Muenchen |
haftmann@28440 | 4 |
|
haftmann@28440 | 5 |
More antiquotations. |
haftmann@28440 | 6 |
*) |
haftmann@28440 | 7 |
|
haftmann@28440 | 8 |
signature MORE_ANTIQUOTE = |
haftmann@28440 | 9 |
sig |
haftmann@28440 | 10 |
val verbatim_lines: string list -> string |
haftmann@28440 | 11 |
end; |
haftmann@28440 | 12 |
|
haftmann@28440 | 13 |
structure More_Antiquote : MORE_ANTIQUOTE = |
haftmann@28440 | 14 |
struct |
haftmann@28440 | 15 |
|
haftmann@28440 | 16 |
structure O = ThyOutput; |
haftmann@28440 | 17 |
|
haftmann@28440 | 18 |
(* printing verbatim lines *) |
haftmann@28440 | 19 |
|
haftmann@28440 | 20 |
val verbatim_line = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
haftmann@28440 | 21 |
val verbatim_lines = rev |
haftmann@28440 | 22 |
#> dropwhile (fn s => s = "") |
haftmann@28440 | 23 |
#> rev |
haftmann@28440 | 24 |
#> map verbatim_line #> space_implode "\\newline%\n" |
haftmann@28440 | 25 |
#> prefix "\\isaverbatim%\n\\noindent%\n" |
haftmann@28440 | 26 |
|
haftmann@28440 | 27 |
|
haftmann@28440 | 28 |
(* class antiquotation *) |
haftmann@28440 | 29 |
|
haftmann@28440 | 30 |
local |
haftmann@28440 | 31 |
|
haftmann@28634 | 32 |
val pr_text = enclose "\\isa{" "}" o Pretty.output o Pretty.str; |
haftmann@28634 | 33 |
|
haftmann@28634 | 34 |
fun pr_class ctxt = Sign.read_class (ProofContext.theory_of ctxt) |
haftmann@28634 | 35 |
#> Sign.extern_class (ProofContext.theory_of ctxt) |
haftmann@28634 | 36 |
#> pr_text; |
haftmann@28634 | 37 |
|
haftmann@28634 | 38 |
fun pr_type ctxt = Sign.intern_type (ProofContext.theory_of ctxt) |
haftmann@28634 | 39 |
#> tap (Sign.arity_number (ProofContext.theory_of ctxt)) |
haftmann@28634 | 40 |
#> Sign.extern_type (ProofContext.theory_of ctxt) |
haftmann@28634 | 41 |
#> pr_text; |
haftmann@28440 | 42 |
|
haftmann@28440 | 43 |
in |
haftmann@28440 | 44 |
|
haftmann@28440 | 45 |
val _ = O.add_commands |
haftmann@28634 | 46 |
[("class", ThyOutput.args (Scan.lift Args.name) (K pr_class)), |
haftmann@28634 | 47 |
("type", ThyOutput.args (Scan.lift Args.name) (K pr_type))] |
haftmann@28440 | 48 |
|
haftmann@28440 | 49 |
end; |
haftmann@28440 | 50 |
|
haftmann@28440 | 51 |
|
haftmann@28440 | 52 |
(* code antiquotation *) |
haftmann@28440 | 53 |
|
haftmann@28440 | 54 |
local |
haftmann@28440 | 55 |
|
haftmann@28440 | 56 |
val parse_const_terms = Scan.repeat1 Args.term |
haftmann@28440 | 57 |
>> (fn ts => fn thy => map (Code_Unit.check_const thy) ts); |
haftmann@28440 | 58 |
val parse_consts = Scan.lift (Args.parens (Args.$$$ "consts")) |-- parse_const_terms |
haftmann@28679 | 59 |
>> (fn mk_cs => fn thy => fn naming => map (the o Code_Thingol.lookup_const naming) (mk_cs thy)); |
haftmann@28440 | 60 |
val parse_types = Scan.lift (Args.parens (Args.$$$ "types") |-- Scan.repeat1 Args.name) |
haftmann@28679 | 61 |
>> (fn tycos => fn thy => fn naming => map (the o Code_Thingol.lookup_tyco naming o Sign.intern_type thy) tycos); |
haftmann@28440 | 62 |
val parse_classes = Scan.lift (Args.parens (Args.$$$ "classes") |-- Scan.repeat1 Args.name) |
haftmann@28679 | 63 |
>> (fn classes => fn thy => fn naming => map (the o Code_Thingol.lookup_class naming o Sign.intern_class thy) classes); |
haftmann@28440 | 64 |
val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name)) |
haftmann@28679 | 65 |
>> (fn insts => fn thy => fn naming => map (the o Code_Thingol.lookup_instance naming o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts); |
haftmann@28440 | 66 |
val parse_names = parse_consts || parse_types || parse_classes || parse_instances; |
haftmann@28440 | 67 |
|
haftmann@28440 | 68 |
fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) = |
haftmann@28440 | 69 |
Code_Target.code_of (ProofContext.theory_of ctxt) |
haftmann@28440 | 70 |
target "Example" (mk_cs (ProofContext.theory_of ctxt)) |
haftmann@28679 | 71 |
(fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss) |
haftmann@28440 | 72 |
|> split_lines |
haftmann@28440 | 73 |
|> verbatim_lines; |
haftmann@28440 | 74 |
|
haftmann@28440 | 75 |
in |
haftmann@28440 | 76 |
|
haftmann@28440 | 77 |
val _ = O.add_commands |
haftmann@28440 | 78 |
[("code_stmts", O.args |
haftmann@28440 | 79 |
(parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name)) |
haftmann@28440 | 80 |
code_stmts)] |
haftmann@28440 | 81 |
|
haftmann@28440 | 82 |
end |
haftmann@28440 | 83 |
|
haftmann@28440 | 84 |
end; |