6 |
6 |
7 structure Pure_Syn: sig end = |
7 structure Pure_Syn: sig end = |
8 struct |
8 struct |
9 |
9 |
10 val _ = |
10 val _ = |
11 Outer_Syntax.markup_command Outer_Syntax.Markup ("header", @{here}) "theory header" |
11 Outer_Syntax.command ("header", @{here}) "theory header" |
12 (Parse.document_source >> Thy_Output.header_markup); |
12 (Parse.document_source >> Thy_Output.old_header_command); |
13 |
13 |
14 val _ = |
14 val _ = |
15 Outer_Syntax.markup_command Outer_Syntax.Markup ("chapter", @{here}) "chapter heading" |
15 Outer_Syntax.command ("chapter", @{here}) "chapter heading" |
16 (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup); |
16 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command); |
17 |
17 |
18 val _ = |
18 val _ = |
19 Outer_Syntax.markup_command Outer_Syntax.Markup ("section", @{here}) "section heading" |
19 Outer_Syntax.command ("section", @{here}) "section heading" |
20 (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup); |
20 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command); |
21 |
21 |
22 val _ = |
22 val _ = |
23 Outer_Syntax.markup_command Outer_Syntax.Markup ("subsection", @{here}) "subsection heading" |
23 Outer_Syntax.command ("subsection", @{here}) "subsection heading" |
24 (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup); |
24 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command); |
25 |
25 |
26 val _ = |
26 val _ = |
27 Outer_Syntax.markup_command Outer_Syntax.Markup ("subsubsection", @{here}) "subsubsection heading" |
27 Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading" |
28 (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup); |
28 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command); |
|
29 |
|
30 val _ = |
|
31 Outer_Syntax.command ("text", @{here}) "formal comment (primary style)" |
|
32 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command); |
|
33 |
|
34 val _ = |
|
35 Outer_Syntax.command ("txt", @{here}) "formal comment (secondary style)" |
|
36 (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command); |
|
37 |
|
38 val _ = |
|
39 Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text" |
|
40 (Parse.document_source >> K (Toplevel.imperative I)); |
29 |
41 |
30 val _ = |
42 val _ = |
31 Outer_Syntax.command ("theory", @{here}) "begin theory" |
43 Outer_Syntax.command ("theory", @{here}) "begin theory" |
32 (Thy_Header.args >> |
44 (Thy_Header.args >> |
33 (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization"))); |
45 (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization"))); |