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_list function from ThyOutput in order to *) |
6 (* enable the option [gray] *) |
6 (* enable the options [gray, linenos] *) |
7 |
7 |
8 val gray = ref false; |
8 val gray = ref false; |
|
9 val linenos = ref false |
9 |
10 |
10 fun boolean "" = true |
11 fun boolean "" = true |
11 | boolean "true" = true |
12 | boolean "true" = true |
12 | boolean "false" = false |
13 | boolean "false" = false |
13 | boolean s = error ("Bad boolean value: " ^ quote s); |
14 | boolean s = error ("Bad boolean value: " ^ quote s); |
18 |> (if ! ThyOutput.quotes then map Pretty.quote else I) |
19 |> (if ! ThyOutput.quotes then map Pretty.quote else I) |
19 |> (if ! ThyOutput.display then |
20 |> (if ! ThyOutput.display then |
20 map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) |
21 map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) |
21 #> space_implode "\\isasep\\isanewline%\n" |
22 #> space_implode "\\isasep\\isanewline%\n" |
22 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
23 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
|
24 #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) |
23 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
25 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
24 else |
26 else |
25 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
27 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
26 #> space_implode "\\isasep\\isanewline%\n" |
28 #> space_implode "\\isasep\\isanewline%\n" |
27 #> enclose "\\isa{" "}"); |
29 #> enclose "\\isa{" "}"); |
28 |
30 |
29 fun output pretty src ctxt = output_list pretty src ctxt o single |
31 fun output pretty src ctxt = output_list pretty src ctxt o single |
30 |
32 |
31 val _ = ThyOutput.add_options |
33 val _ = ThyOutput.add_options |
32 [("gray", Library.setmp gray o boolean)] |
34 [("gray", Library.setmp gray o boolean), |
|
35 ("linenos", Library.setmp linenos o boolean)] |
33 |
36 |
34 |
37 |
35 |
38 |
36 |
39 |
37 (** theory data **) |
40 (** theory data **) |