5 More antiquotations. |
5 More antiquotations. |
6 *) |
6 *) |
7 |
7 |
8 signature MORE_ANTIQUOTE = |
8 signature MORE_ANTIQUOTE = |
9 sig |
9 sig |
10 val verbatim_lines: string list -> string |
10 val verbatim: string -> string |
11 end; |
11 end; |
12 |
12 |
13 structure More_Antiquote : MORE_ANTIQUOTE = |
13 structure More_Antiquote : MORE_ANTIQUOTE = |
14 struct |
14 struct |
15 |
15 |
16 structure O = ThyOutput; |
16 structure O = ThyOutput; |
17 |
17 |
18 (* printing verbatim lines *) |
18 (* printing verbatim lines *) |
19 |
19 |
20 val verbatim_line = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
20 fun verbatim s = |
21 val verbatim_lines = rev |
21 let |
22 #> dropwhile (fn s => s = "") |
22 val parse = Scan.repeat |
23 #> rev |
23 (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}" |
24 #> map verbatim_line #> space_implode "\\newline%\n" |
24 || (Scan.this_string " " |
25 #> prefix "\\isaverbatim%\n\\noindent%\n" |
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 |
26 |
48 |
27 |
49 |
28 (* class antiquotation *) |
50 (* class antiquotation *) |
29 |
51 |
30 local |
52 local |
67 |
89 |
68 fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) = |
90 fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) = |
69 Code_Target.code_of (ProofContext.theory_of ctxt) |
91 Code_Target.code_of (ProofContext.theory_of ctxt) |
70 target "Example" (mk_cs (ProofContext.theory_of ctxt)) |
92 target "Example" (mk_cs (ProofContext.theory_of ctxt)) |
71 (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss) |
93 (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss) |
72 |> split_lines |
94 |> verbatim; |
73 |> verbatim_lines; |
|
74 |
95 |
75 in |
96 in |
76 |
97 |
77 val _ = O.add_commands |
98 val _ = O.add_commands |
78 [("code_stmts", O.args |
99 [("code_stmts", O.args |