49 val quotes_default = Unsynchronized.ref false; |
49 val quotes_default = Unsynchronized.ref false; |
50 val indent_default = Unsynchronized.ref 0; |
50 val indent_default = Unsynchronized.ref 0; |
51 val source_default = Unsynchronized.ref false; |
51 val source_default = Unsynchronized.ref false; |
52 val break_default = Unsynchronized.ref false; |
52 val break_default = Unsynchronized.ref false; |
53 |
53 |
54 val (display, setup_display) = Attrib.config_bool "thy_output_display" (fn _ => ! display_default); |
54 val display = Attrib.setup_config_bool (Binding.name "thy_output_display") (fn _ => ! display_default); |
55 val (quotes, setup_quotes) = Attrib.config_bool "thy_output_quotes" (fn _ => ! quotes_default); |
55 val quotes = Attrib.setup_config_bool (Binding.name "thy_output_quotes") (fn _ => ! quotes_default); |
56 val (indent, setup_indent) = Attrib.config_int "thy_output_indent" (fn _ => ! indent_default); |
56 val indent = Attrib.setup_config_int (Binding.name "thy_output_indent") (fn _ => ! indent_default); |
57 val (source, setup_source) = Attrib.config_bool "thy_output_source" (fn _ => ! source_default); |
57 val source = Attrib.setup_config_bool (Binding.name "thy_output_source") (fn _ => ! source_default); |
58 val (break, setup_break) = Attrib.config_bool "thy_output_break" (fn _ => ! break_default); |
58 val break = Attrib.setup_config_bool (Binding.name "thy_output_break") (fn _ => ! break_default); |
59 |
|
60 val _ = Context.>> (Context.map_theory |
|
61 (setup_display #> setup_quotes #> setup_indent #> setup_source #> setup_break)); |
|
62 |
59 |
63 |
60 |
64 structure Wrappers = Proof_Data |
61 structure Wrappers = Proof_Data |
65 ( |
62 ( |
66 type T = ((unit -> string) -> unit -> string) list; |
63 type T = ((unit -> string) -> unit -> string) list; |