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