41 structure Document_Antiquotation: DOCUMENT_ANTIQUOTATION = |
41 structure Document_Antiquotation: DOCUMENT_ANTIQUOTATION = |
42 struct |
42 struct |
43 |
43 |
44 (* options *) |
44 (* options *) |
45 |
45 |
46 val thy_output_display = Attrib.setup_option_bool ("thy_output_display", \<^here>); |
46 val thy_output_display = Attrib.setup_option_bool (\<^system_option>\<open>thy_output_display\<close>, \<^here>); |
47 val thy_output_break = Attrib.setup_option_bool ("thy_output_break", \<^here>); |
47 val thy_output_break = Attrib.setup_option_bool (\<^system_option>\<open>thy_output_break\<close>, \<^here>); |
48 val thy_output_cartouche = Attrib.setup_option_bool ("thy_output_cartouche", \<^here>); |
48 val thy_output_cartouche = Attrib.setup_option_bool (\<^system_option>\<open>thy_output_cartouche\<close>, \<^here>); |
49 val thy_output_quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>); |
49 val thy_output_quotes = Attrib.setup_option_bool (\<^system_option>\<open>thy_output_quotes\<close>, \<^here>); |
50 val thy_output_margin = Attrib.setup_option_int ("thy_output_margin", \<^here>); |
50 val thy_output_margin = Attrib.setup_option_int (\<^system_option>\<open>thy_output_margin\<close>, \<^here>); |
51 val thy_output_indent = Attrib.setup_option_int ("thy_output_indent", \<^here>); |
51 val thy_output_indent = Attrib.setup_option_int (\<^system_option>\<open>thy_output_indent\<close>, \<^here>); |
52 val thy_output_source = Attrib.setup_option_bool ("thy_output_source", \<^here>); |
52 val thy_output_source = Attrib.setup_option_bool (\<^system_option>\<open>thy_output_source\<close>, \<^here>); |
53 val thy_output_source_cartouche = Attrib.setup_option_bool ("thy_output_source_cartouche", \<^here>); |
53 val thy_output_source_cartouche = Attrib.setup_option_bool (\<^system_option>\<open>thy_output_source_cartouche\<close>, \<^here>); |
54 val thy_output_modes = Attrib.setup_option_string ("thy_output_modes", \<^here>); |
54 val thy_output_modes = Attrib.setup_option_string (\<^system_option>\<open>thy_output_modes\<close>, \<^here>); |
55 |
55 |
56 |
56 |
57 (* blanks *) |
57 (* blanks *) |
58 |
58 |
59 fun trim_blanks ctxt = |
59 fun trim_blanks ctxt = |