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 |
11 |
11 |
12 fun output txt = |
12 fun output ctxt 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 ! Thy_Output.quotes then map Pretty.quote else I) |
17 |> (if Config.get ctxt Thy_Output.quotes then map Pretty.quote else I) |
18 |> (if ! Thy_Output.display then |
18 |> (if Config.get ctxt Thy_Output.display then |
19 map (Output.output o Pretty.string_of o Pretty.indent (! Thy_Output.indent)) |
19 map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt 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 ! Thy_Output.break then Pretty.string_of else Pretty.str_of)) |
25 map (Output.output o (if Config.get ctxt 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 = |
72 fun get_str_index {main = m, minor = n} = |
72 fun get_str_index {main = m, minor = n} = |
73 (case n of |
73 (case n of |
74 Struct s => implode ["\\index[str]{{\\tt\\slshape{}", get_word s, "}!", get_indstring m, "}"] |
74 Struct s => implode ["\\index[str]{{\\tt\\slshape{}", get_word s, "}!", get_indstring m, "}"] |
75 | _ => "") |
75 | _ => "") |
76 |
76 |
77 fun output_indexed ind txt = |
77 fun output_indexed ctxt ind txt = |
78 txt |> output |
78 txt |> output ctxt |
79 |> prefix (get_index ind) |
79 |> prefix (get_index ind) |
80 |> prefix (get_str_index ind) |
80 |> prefix (get_str_index ind) |
81 |
81 |
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 _ = Thy_Output.add_options |
87 val _ = Thy_Output.add_option "gray" |
88 [("gray", Library.setmp_CRITICAL gray o boolean), |
88 (Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean) |
89 ("linenos", Library.setmp_CRITICAL linenos o boolean)] |
89 val _ = Thy_Output.add_option "linenos" |
|
90 (Thy_Output.add_wrapper o Library.setmp_CRITICAL linenos o boolean) |
90 |
91 |
91 end |
92 end |