author | haftmann |
Mon, 10 Nov 2008 09:03:28 +0100 | |
changeset 28727 | 185110a4b97a |
parent 28714 | 1992553cccfe |
child 28921 | e60a41c21768 |
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@28727 | 10 |
val typewriter: string -> 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@28727 | 18 |
(* printing typewriter lines *) |
haftmann@28440 | 19 |
|
haftmann@28727 | 20 |
fun typewriter s = |
haftmann@28714 | 21 |
let |
haftmann@28714 | 22 |
val parse = Scan.repeat |
haftmann@28714 | 23 |
(Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}" |
haftmann@28714 | 24 |
|| (Scan.this_string " " |
haftmann@28714 | 25 |
|| Scan.this_string ":" |
haftmann@28714 | 26 |
|| Scan.this_string "\"" |-- Scan.succeed "{\\char34}" |
haftmann@28714 | 27 |
|| Scan.this_string "#" |-- Scan.succeed "{\\char35}" |
haftmann@28714 | 28 |
|| Scan.this_string "$" |-- Scan.succeed "{\\char36}" |
haftmann@28714 | 29 |
|| Scan.this_string "%" |-- Scan.succeed "{\\char37}" |
haftmann@28714 | 30 |
|| Scan.this_string "&" |-- Scan.succeed "{\\char38}" |
haftmann@28714 | 31 |
|| Scan.this_string "\\" |-- Scan.succeed "{\\char92}" |
haftmann@28714 | 32 |
|| Scan.this_string "^" |-- Scan.succeed "{\\char94}" |
haftmann@28714 | 33 |
|| Scan.this_string "_" |-- Scan.succeed "{\\char95}" |
haftmann@28714 | 34 |
|| Scan.this_string "{" |-- Scan.succeed "{\\char123}" |
haftmann@28714 | 35 |
|| Scan.this_string "}" |-- Scan.succeed "{\\char125}" |
haftmann@28714 | 36 |
|| Scan.this_string "~" |-- Scan.succeed "{\\char126}") |
haftmann@28714 | 37 |
-- Scan.repeat (Scan.this_string " ") |
haftmann@28714 | 38 |
>> (fn (x, xs) => x ^ replicate_string (length xs) "~") |
haftmann@28714 | 39 |
|| Scan.one Symbol.not_eof); |
haftmann@28714 | 40 |
fun is_newline s = (s = "\n"); |
haftmann@28714 | 41 |
val cs = explode s |> take_prefix is_newline |> snd |
haftmann@28714 | 42 |
|> take_suffix is_newline |> fst; |
haftmann@28714 | 43 |
val (texts, []) = Scan.finite Symbol.stopper parse cs |
haftmann@28714 | 44 |
in if null texts |
haftmann@28714 | 45 |
then "" |
haftmann@28727 | 46 |
else implode ("\\isatypewriter%\n\\noindent%\n\\hspace*{0pt}" :: texts) |
haftmann@28714 | 47 |
end |
haftmann@28440 | 48 |
|
haftmann@28440 | 49 |
|
haftmann@28440 | 50 |
(* class antiquotation *) |
haftmann@28440 | 51 |
|
haftmann@28440 | 52 |
local |
haftmann@28440 | 53 |
|
haftmann@28634 | 54 |
val pr_text = enclose "\\isa{" "}" o Pretty.output o Pretty.str; |
haftmann@28634 | 55 |
|
haftmann@28634 | 56 |
fun pr_class ctxt = Sign.read_class (ProofContext.theory_of ctxt) |
haftmann@28634 | 57 |
#> Sign.extern_class (ProofContext.theory_of ctxt) |
haftmann@28634 | 58 |
#> pr_text; |
haftmann@28634 | 59 |
|
haftmann@28634 | 60 |
fun pr_type ctxt = Sign.intern_type (ProofContext.theory_of ctxt) |
haftmann@28634 | 61 |
#> tap (Sign.arity_number (ProofContext.theory_of ctxt)) |
haftmann@28634 | 62 |
#> Sign.extern_type (ProofContext.theory_of ctxt) |
haftmann@28634 | 63 |
#> pr_text; |
haftmann@28440 | 64 |
|
haftmann@28440 | 65 |
in |
haftmann@28440 | 66 |
|
haftmann@28440 | 67 |
val _ = O.add_commands |
haftmann@28634 | 68 |
[("class", ThyOutput.args (Scan.lift Args.name) (K pr_class)), |
haftmann@28634 | 69 |
("type", ThyOutput.args (Scan.lift Args.name) (K pr_type))] |
haftmann@28440 | 70 |
|
haftmann@28440 | 71 |
end; |
haftmann@28440 | 72 |
|
haftmann@28440 | 73 |
|
haftmann@28440 | 74 |
(* code antiquotation *) |
haftmann@28440 | 75 |
|
haftmann@28440 | 76 |
local |
haftmann@28440 | 77 |
|
haftmann@28440 | 78 |
val parse_const_terms = Scan.repeat1 Args.term |
haftmann@28440 | 79 |
>> (fn ts => fn thy => map (Code_Unit.check_const thy) ts); |
haftmann@28440 | 80 |
val parse_consts = Scan.lift (Args.parens (Args.$$$ "consts")) |-- parse_const_terms |
haftmann@28679 | 81 |
>> (fn mk_cs => fn thy => fn naming => map (the o Code_Thingol.lookup_const naming) (mk_cs thy)); |
haftmann@28440 | 82 |
val parse_types = Scan.lift (Args.parens (Args.$$$ "types") |-- Scan.repeat1 Args.name) |
haftmann@28679 | 83 |
>> (fn tycos => fn thy => fn naming => map (the o Code_Thingol.lookup_tyco naming o Sign.intern_type thy) tycos); |
haftmann@28440 | 84 |
val parse_classes = Scan.lift (Args.parens (Args.$$$ "classes") |-- Scan.repeat1 Args.name) |
haftmann@28679 | 85 |
>> (fn classes => fn thy => fn naming => map (the o Code_Thingol.lookup_class naming o Sign.intern_class thy) classes); |
haftmann@28440 | 86 |
val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name)) |
haftmann@28679 | 87 |
>> (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 | 88 |
val parse_names = parse_consts || parse_types || parse_classes || parse_instances; |
haftmann@28440 | 89 |
|
haftmann@28440 | 90 |
fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) = |
haftmann@28440 | 91 |
Code_Target.code_of (ProofContext.theory_of ctxt) |
haftmann@28440 | 92 |
target "Example" (mk_cs (ProofContext.theory_of ctxt)) |
haftmann@28679 | 93 |
(fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss) |
haftmann@28727 | 94 |
|> typewriter; |
haftmann@28440 | 95 |
|
haftmann@28440 | 96 |
in |
haftmann@28440 | 97 |
|
haftmann@28440 | 98 |
val _ = O.add_commands |
haftmann@28440 | 99 |
[("code_stmts", O.args |
haftmann@28440 | 100 |
(parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name)) |
haftmann@28440 | 101 |
code_stmts)] |
haftmann@28440 | 102 |
|
haftmann@28440 | 103 |
end |
haftmann@28440 | 104 |
|
haftmann@28440 | 105 |
end; |