equal
deleted
inserted
replaced
|
1 |
1 structure Chunks = |
2 structure Chunks = |
2 struct |
3 struct |
|
4 |
|
5 (* rebuilding the output_list function from ThyOutput in order to *) |
|
6 (* enable the option [gray] *) |
|
7 |
|
8 val gray = ref false; |
|
9 |
|
10 fun boolean "" = true |
|
11 | boolean "true" = true |
|
12 | boolean "false" = false |
|
13 | boolean s = error ("Bad boolean value: " ^ quote s); |
|
14 |
|
15 fun output_list pretty src ctxt xs = |
|
16 map (pretty ctxt) xs (*always pretty in order to exhibit errors!*) |
|
17 |> (if ! ThyOutput.source then K [ThyOutput.pretty_text (ThyOutput.str_of_source src)] else I) |
|
18 |> (if ! ThyOutput.quotes then map Pretty.quote else I) |
|
19 |> (if ! ThyOutput.display then |
|
20 map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) |
|
21 #> space_implode "\\isasep\\isanewline%\n" |
|
22 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
|
23 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
|
24 else |
|
25 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
|
26 #> space_implode "\\isasep\\isanewline%\n" |
|
27 #> enclose "\\isa{" "}"); |
|
28 |
|
29 val _ = ThyOutput.add_options |
|
30 [("gray", Library.setmp gray o boolean)] |
3 |
31 |
4 (** theory data **) |
32 (** theory data **) |
5 |
33 |
6 structure ChunkData = TheoryDataFun |
34 structure ChunkData = TheoryDataFun |
7 ( |
35 ( |
123 else ("", tok :: toks''') |
151 else ("", tok :: toks''') |
124 end) |
152 end) |
125 val txt = spc ^ implode (transform_cmts toks') |
153 val txt = spc ^ implode (transform_cmts toks') |
126 in |
154 in |
127 txt |> split_lines |> |
155 txt |> split_lines |> |
128 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
156 output_list (fn _ => fn s => Pretty.str s) src ctxt |
129 end; |
157 end; |
130 |
158 |
131 val _ = ThyOutput.add_commands |
159 val _ = ThyOutput.add_commands |
132 [("ML_chunk", ThyOutput.args (Scan.lift Args.name) output_chunk)]; |
160 [("ML_chunk", ThyOutput.args (Scan.lift Args.name) output_chunk)]; |
133 |
161 |