equal
deleted
inserted
replaced
1 |
1 |
2 structure OutputTutorial = |
2 structure OutputTutorial = |
3 struct |
3 struct |
4 |
4 |
5 (* rebuilding the output function from ThyOutput in order to *) |
5 (* rebuilding the output function from Thy_Output in order to *) |
6 (* enable the options [gray, linenos] *) |
6 (* enable the options [gray, linenos] *) |
7 |
7 |
8 val gray = Unsynchronized.ref false |
8 val gray = Unsynchronized.ref false |
9 val linenos = Unsynchronized.ref false |
9 val linenos = Unsynchronized.ref false |
10 |
10 |
12 fun output txt = |
12 fun output txt = |
13 let |
13 let |
14 val prts = map Pretty.str txt |
14 val prts = map Pretty.str txt |
15 in |
15 in |
16 prts |
16 prts |
17 |> (if ! ThyOutput.quotes then map Pretty.quote else I) |
17 |> (if ! Thy_Output.quotes then map Pretty.quote else I) |
18 |> (if ! ThyOutput.display then |
18 |> (if ! Thy_Output.display then |
19 map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) |
19 map (Output.output o Pretty.string_of o Pretty.indent (! Thy_Output.indent)) |
20 #> space_implode "\\isasep\\isanewline%\n" |
20 #> space_implode "\\isasep\\isanewline%\n" |
21 #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) |
21 #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) |
22 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
22 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
23 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
23 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
24 else |
24 else |
25 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
25 map (Output.output o (if ! Thy_Output.break then Pretty.string_of else Pretty.str_of)) |
26 #> space_implode "\\isasep\\isanewline%\n" |
26 #> space_implode "\\isasep\\isanewline%\n" |
27 #> enclose "\\isa{" "}") |
27 #> enclose "\\isa{" "}") |
28 end |
28 end |
29 |
29 |
30 datatype indstring = |
30 datatype indstring = |
82 fun boolean "" = true |
82 fun boolean "" = true |
83 | boolean "true" = true |
83 | boolean "true" = true |
84 | boolean "false" = false |
84 | boolean "false" = false |
85 | boolean s = error ("Bad boolean value: " ^ quote s); |
85 | boolean s = error ("Bad boolean value: " ^ quote s); |
86 |
86 |
87 val _ = ThyOutput.add_options |
87 val _ = Thy_Output.add_options |
88 [("gray", Library.setmp_CRITICAL gray o boolean), |
88 [("gray", Library.setmp_CRITICAL gray o boolean), |
89 ("linenos", Library.setmp_CRITICAL linenos o boolean)] |
89 ("linenos", Library.setmp_CRITICAL linenos o boolean)] |
90 |
90 |
91 end |
91 end |