equal
deleted
inserted
replaced
1 |
1 |
2 structure Chunks = |
2 structure Chunks = |
3 struct |
3 struct |
4 |
|
5 (* rebuilding the output function from ThyOutput in order to *) |
|
6 (* enable the options [gray, linenos] *) |
|
7 |
|
8 val gray = ref false; |
|
9 val linenos = ref false |
|
10 |
|
11 fun output prts = |
|
12 prts |
|
13 |> (if ! ThyOutput.quotes then map Pretty.quote else I) |
|
14 |> (if ! ThyOutput.display then |
|
15 map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) |
|
16 #> space_implode "\\isasep\\isanewline%\n" |
|
17 #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) |
|
18 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
|
19 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
|
20 else |
|
21 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
|
22 #> space_implode "\\isasep\\isanewline%\n" |
|
23 #> enclose "\\isa{" "}"); |
|
24 |
|
25 |
|
26 fun boolean "" = true |
|
27 | boolean "true" = true |
|
28 | boolean "false" = false |
|
29 | boolean s = error ("Bad boolean value: " ^ quote s); |
|
30 |
|
31 val _ = ThyOutput.add_options |
|
32 [("gray", Library.setmp gray o boolean), |
|
33 ("linenos", Library.setmp linenos o boolean)] |
|
34 |
|
35 |
|
36 |
|
37 |
4 |
38 (** theory data **) |
5 (** theory data **) |
39 |
6 |
40 structure ChunkData = TheoryDataFun |
7 structure ChunkData = TheoryDataFun |
41 ( |
8 ( |
156 toks''') |
123 toks''') |
157 else ("", tok :: toks''') |
124 else ("", tok :: toks''') |
158 end) |
125 end) |
159 val txt = spc ^ implode (transform_cmts toks') |
126 val txt = spc ^ implode (transform_cmts toks') |
160 in |
127 in |
161 txt |> split_lines |> |
128 txt |> split_lines |> OutputFN.output |
162 (map Pretty.str) |> output |
|
163 end; |
129 end; |
164 |
130 |
165 val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk; |
131 val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk; |
166 |
132 |
167 end; |
133 end; |