3 struct |
3 struct |
4 |
4 |
5 (* rebuilding the output function from Thy_Output 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 thy_output_linenos = Attrib.setup_config_bool @{binding linenos} (K false) |
9 val linenos = Unsynchronized.ref false |
9 val thy_output_gray = Attrib.setup_config_bool @{binding gray} (K false) |
10 |
10 |
11 |
11 fun output_raw ctxt txt = |
12 fun output ctxt txt = |
|
13 let |
12 let |
14 val prts = map Pretty.str txt |
13 val prts = map Pretty.str txt |
15 in |
14 in |
16 prts |
15 prts |
17 |> (if Config.get ctxt Thy_Output.quotes then map Pretty.quote else I) |
16 |> (if Config.get ctxt Document_Antiquotation.thy_output_quotes then map Pretty.quote else I) |
18 |> (if Config.get ctxt Thy_Output.display then |
17 |> (if Config.get ctxt Document_Antiquotation.thy_output_display then |
19 map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt Thy_Output.indent)) |
18 map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent)) |
20 #> space_implode "\\isasep\\isanewline%\n" |
19 #> space_implode "\\isasep\\isanewline%\n" |
21 #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) |
20 #> (if Config.get ctxt thy_output_linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) |
22 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
21 #> (if Config.get ctxt thy_output_gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
23 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
22 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
24 else |
23 else |
25 map (Output.output o (if Config.get ctxt Thy_Output.break then Pretty.string_of else Pretty.str_of)) |
24 map (Output.output o (if Config.get ctxt Document_Antiquotation.thy_output_break then Pretty.string_of else Pretty.unformatted_string_of)) |
26 #> space_implode "\\isasep\\isanewline%\n" |
25 #> space_implode "\\isasep\\isanewline%\n" |
27 #> enclose "\\isa{" "}") |
26 #> enclose "\\isa{" "}") |
28 end |
27 end |
|
28 |
|
29 fun output ctxt txt = Latex.string (output_raw ctxt txt) |
29 |
30 |
30 datatype indstring = |
31 datatype indstring = |
31 NoString |
32 NoString |
32 | Plain of string |
33 | Plain of string |
33 | Code of string |
34 | Code of string |
73 (case n of |
74 (case n of |
74 Struct s => implode ["\\index[str]{{\\tt\\slshape{}", get_word s, "}!", get_indstring m, "}"] |
75 Struct s => implode ["\\index[str]{{\\tt\\slshape{}", get_word s, "}!", get_indstring m, "}"] |
75 | _ => "") |
76 | _ => "") |
76 |
77 |
77 fun output_indexed ctxt ind txt = |
78 fun output_indexed ctxt ind txt = |
78 txt |> output ctxt |
79 txt |> output_raw ctxt |
79 |> prefix (get_index ind) |
80 |> prefix (get_index ind) |
80 |> prefix (get_str_index ind) |
81 |> prefix (get_str_index ind) |
|
82 |> Latex.string |
81 |
83 |
82 fun boolean "" = true |
84 fun boolean "" = true |
83 | boolean "true" = true |
85 | boolean "true" = true |
84 | boolean "false" = false |
86 | boolean "false" = false |
85 | boolean s = error ("Bad boolean value: " ^ quote s); |
87 | boolean s = error ("Bad boolean value: " ^ quote s); |
86 |
88 |
87 val gray_setup = Thy_Output.add_option @{binding "gray"} |
89 val _ = Theory.setup |
88 (Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean) |
90 (Document_Antiquotation.setup_option @{binding gray} (Config.put thy_output_gray o boolean) #> |
89 val linenos_setup = Thy_Output.add_option @{binding "linenos"} |
91 Document_Antiquotation.setup_option @{binding linenos} (Config.put thy_output_linenos o boolean) ); |
90 (Thy_Output.add_wrapper o Library.setmp_CRITICAL linenos o boolean) |
|
91 |
92 |
92 val setup = |
|
93 gray_setup #> |
|
94 linenos_setup |
|
95 |
93 |
96 end |
94 end |