author | haftmann |
Thu, 02 Oct 2008 17:18:22 +0200 | |
changeset 28461 | 640b7f8f9cad |
parent 28440 | 0b9ddfa6458e |
child 28634 | 764ef122a164 |
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@28461 | 32 |
fun pr_class ctxt = enclose "\\isa{" "}" o Pretty.output o Pretty.str |
haftmann@28461 | 33 |
o Sign.extern_class (ProofContext.theory_of ctxt) o Sign.read_class (ProofContext.theory_of ctxt); |
haftmann@28440 | 34 |
|
haftmann@28440 | 35 |
in |
haftmann@28440 | 36 |
|
haftmann@28440 | 37 |
val _ = O.add_commands |
haftmann@28440 | 38 |
[("class", ThyOutput.args (Scan.lift Args.name) (K pr_class))] |
haftmann@28440 | 39 |
|
haftmann@28440 | 40 |
end; |
haftmann@28440 | 41 |
|
haftmann@28440 | 42 |
|
haftmann@28440 | 43 |
(* code antiquotation *) |
haftmann@28440 | 44 |
|
haftmann@28440 | 45 |
local |
haftmann@28440 | 46 |
|
haftmann@28440 | 47 |
val parse_const_terms = Scan.repeat1 Args.term |
haftmann@28440 | 48 |
>> (fn ts => fn thy => map (Code_Unit.check_const thy) ts); |
haftmann@28440 | 49 |
val parse_consts = Scan.lift (Args.parens (Args.$$$ "consts")) |-- parse_const_terms |
haftmann@28440 | 50 |
>> (fn mk_cs => fn thy => map (Code_Name.const thy) (mk_cs thy)); |
haftmann@28440 | 51 |
val parse_types = Scan.lift (Args.parens (Args.$$$ "types") |-- Scan.repeat1 Args.name) |
haftmann@28440 | 52 |
>> (fn tycos => fn thy => map (Code_Name.tyco thy o Sign.intern_type thy) tycos); |
haftmann@28440 | 53 |
val parse_classes = Scan.lift (Args.parens (Args.$$$ "classes") |-- Scan.repeat1 Args.name) |
haftmann@28440 | 54 |
>> (fn classes => fn thy => map (Code_Name.class thy o Sign.intern_class thy) classes); |
haftmann@28440 | 55 |
val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name)) |
haftmann@28440 | 56 |
>> (fn insts => fn thy => map (Code_Name.instance thy o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts); |
haftmann@28440 | 57 |
val parse_names = parse_consts || parse_types || parse_classes || parse_instances; |
haftmann@28440 | 58 |
|
haftmann@28440 | 59 |
fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) = |
haftmann@28440 | 60 |
Code_Target.code_of (ProofContext.theory_of ctxt) |
haftmann@28440 | 61 |
target "Example" (mk_cs (ProofContext.theory_of ctxt)) |
haftmann@28440 | 62 |
(maps (fn f => f (ProofContext.theory_of ctxt)) mk_stmtss) |
haftmann@28440 | 63 |
|> split_lines |
haftmann@28440 | 64 |
|> verbatim_lines; |
haftmann@28440 | 65 |
|
haftmann@28440 | 66 |
in |
haftmann@28440 | 67 |
|
haftmann@28440 | 68 |
val _ = O.add_commands |
haftmann@28440 | 69 |
[("code_stmts", O.args |
haftmann@28440 | 70 |
(parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name)) |
haftmann@28440 | 71 |
code_stmts)] |
haftmann@28440 | 72 |
|
haftmann@28440 | 73 |
end |
haftmann@28440 | 74 |
|
haftmann@28440 | 75 |
end; |