17 Outer_Syntax.command ("header", @{here}) "theory header" |
17 Outer_Syntax.command ("header", @{here}) "theory header" |
18 (Parse.document_source >> Thy_Output.old_header_command); |
18 (Parse.document_source >> Thy_Output.old_header_command); |
19 |
19 |
20 val _ = |
20 val _ = |
21 Outer_Syntax.command ("chapter", @{here}) "chapter heading" |
21 Outer_Syntax.command ("chapter", @{here}) "chapter heading" |
22 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command); |
22 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false}); |
23 |
23 |
24 val _ = |
24 val _ = |
25 Outer_Syntax.command ("section", @{here}) "section heading" |
25 Outer_Syntax.command ("section", @{here}) "section heading" |
26 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command); |
26 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false}); |
27 |
27 |
28 val _ = |
28 val _ = |
29 Outer_Syntax.command ("subsection", @{here}) "subsection heading" |
29 Outer_Syntax.command ("subsection", @{here}) "subsection heading" |
30 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command); |
30 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false}); |
31 |
31 |
32 val _ = |
32 val _ = |
33 Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading" |
33 Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading" |
34 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command); |
34 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false}); |
35 |
35 |
36 val _ = |
36 val _ = |
37 Outer_Syntax.command ("text", @{here}) "formal comment (primary style)" |
37 Outer_Syntax.command ("text", @{here}) "formal comment (primary style)" |
38 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command); |
38 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true}); |
39 |
39 |
40 val _ = |
40 val _ = |
41 Outer_Syntax.command ("txt", @{here}) "formal comment (secondary style)" |
41 Outer_Syntax.command ("txt", @{here}) "formal comment (secondary style)" |
42 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command); |
42 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true}); |
43 |
43 |
44 val _ = |
44 val _ = |
45 Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text" |
45 Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text" |
46 (Parse.document_source >> (fn s => Toplevel.keep (fn _ => Thy_Output.report_text s))); |
46 (Parse.document_source >> (fn s => Thy_Output.document_command {markdown = true} (NONE, s))); |
47 |
47 |
48 val _ = |
48 val _ = |
49 Outer_Syntax.command ("theory", @{here}) "begin theory" |
49 Outer_Syntax.command ("theory", @{here}) "begin theory" |
50 (Thy_Header.args >> |
50 (Thy_Header.args >> |
51 (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization"))); |
51 (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization"))); |