1 |
1 |
2 structure Chunks = |
2 structure Chunks = |
3 struct |
3 struct |
4 |
4 |
5 (* rebuilding the output_list function from ThyOutput in order to *) |
5 (* rebuilding the output function from ThyOutput in order to *) |
6 (* enable the options [gray, linenos] *) |
6 (* enable the options [gray, linenos] *) |
7 |
7 |
8 val gray = ref false; |
8 val gray = ref false; |
9 val linenos = ref false |
9 val linenos = ref false |
10 |
10 |
11 fun boolean "" = true |
11 fun output prts = |
12 | boolean "true" = true |
12 prts |
13 | boolean "false" = false |
|
14 | boolean s = error ("Bad boolean value: " ^ quote s); |
|
15 |
|
16 fun output_list pretty src ctxt xs = |
|
17 map (pretty ctxt) xs (*always pretty in order to exhibit errors!*) |
|
18 |> (if ! ThyOutput.source then K [ThyOutput.pretty_text (ThyOutput.str_of_source src)] else I) |
|
19 |> (if ! ThyOutput.quotes then map Pretty.quote else I) |
13 |> (if ! ThyOutput.quotes then map Pretty.quote else I) |
20 |> (if ! ThyOutput.display then |
14 |> (if ! ThyOutput.display then |
21 map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) |
15 map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) |
22 #> space_implode "\\isasep\\isanewline%\n" |
16 #> space_implode "\\isasep\\isanewline%\n" |
23 #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) |
17 #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) |
24 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
18 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
25 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
19 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
26 else |
20 else |
27 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
21 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
28 #> space_implode "\\isasep\\isanewline%\n" |
22 #> space_implode "\\isasep\\isanewline%\n" |
29 #> enclose "\\isa{" "}"); |
23 #> enclose "\\isa{" "}"); |
30 |
24 |
31 fun output pretty src ctxt = output_list pretty src ctxt o single |
25 |
|
26 fun boolean "" = true |
|
27 | boolean "true" = true |
|
28 | boolean "false" = false |
|
29 | boolean s = error ("Bad boolean value: " ^ quote s); |
32 |
30 |
33 val _ = ThyOutput.add_options |
31 val _ = ThyOutput.add_options |
34 [("gray", Library.setmp gray o boolean), |
32 [("gray", Library.setmp gray o boolean), |
35 ("linenos", Library.setmp linenos o boolean)] |
33 ("linenos", Library.setmp linenos o boolean)] |
36 |
34 |
159 else ("", tok :: toks''') |
157 else ("", tok :: toks''') |
160 end) |
158 end) |
161 val txt = spc ^ implode (transform_cmts toks') |
159 val txt = spc ^ implode (transform_cmts toks') |
162 in |
160 in |
163 txt |> split_lines |> |
161 txt |> split_lines |> |
164 output_list (fn _ => fn s => Pretty.str s) src ctxt |
162 (map Pretty.str) |> output |
165 end; |
163 end; |
166 |
164 |
167 val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk; |
165 val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk; |
168 |
166 |
169 end; |
167 end; |