45 ("header", Keyword.diag) "theory header" |
45 ("header", Keyword.diag) "theory header" |
46 (Parse.doc_source >> Isar_Cmd.header_markup); |
46 (Parse.doc_source >> Isar_Cmd.header_markup); |
47 |
47 |
48 val _ = |
48 val _ = |
49 Outer_Syntax.markup_command Thy_Output.Markup |
49 Outer_Syntax.markup_command Thy_Output.Markup |
50 ("chapter", Keyword.thy_heading) "chapter heading" |
50 ("chapter", Keyword.thy_heading1) "chapter heading" |
51 (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup); |
51 (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup); |
52 |
52 |
53 val _ = |
53 val _ = |
54 Outer_Syntax.markup_command Thy_Output.Markup |
54 Outer_Syntax.markup_command Thy_Output.Markup |
55 ("section", Keyword.thy_heading) "section heading" |
55 ("section", Keyword.thy_heading2) "section heading" |
56 (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup); |
56 (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup); |
57 |
57 |
58 val _ = |
58 val _ = |
59 Outer_Syntax.markup_command Thy_Output.Markup |
59 Outer_Syntax.markup_command Thy_Output.Markup |
60 ("subsection", Keyword.thy_heading) "subsection heading" |
60 ("subsection", Keyword.thy_heading3) "subsection heading" |
61 (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup); |
61 (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup); |
62 |
62 |
63 val _ = |
63 val _ = |
64 Outer_Syntax.markup_command Thy_Output.Markup |
64 Outer_Syntax.markup_command Thy_Output.Markup |
65 ("subsubsection", Keyword.thy_heading) "subsubsection heading" |
65 ("subsubsection", Keyword.thy_heading4) "subsubsection heading" |
66 (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup); |
66 (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup); |
67 |
67 |
68 val _ = |
68 val _ = |
69 Outer_Syntax.markup_command Thy_Output.MarkupEnv |
69 Outer_Syntax.markup_command Thy_Output.MarkupEnv |
70 ("text", Keyword.thy_decl) "formal comment (theory)" |
70 ("text", Keyword.thy_decl) "formal comment (theory)" |
75 ("text_raw", Keyword.thy_decl) "raw document preparation text" |
75 ("text_raw", Keyword.thy_decl) "raw document preparation text" |
76 (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup); |
76 (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup); |
77 |
77 |
78 val _ = |
78 val _ = |
79 Outer_Syntax.markup_command Thy_Output.Markup |
79 Outer_Syntax.markup_command Thy_Output.Markup |
80 ("sect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)" |
80 ("sect", Keyword.tag_proof Keyword.prf_heading2) "formal comment (proof)" |
81 (Parse.doc_source >> Isar_Cmd.proof_markup); |
81 (Parse.doc_source >> Isar_Cmd.proof_markup); |
82 |
82 |
83 val _ = |
83 val _ = |
84 Outer_Syntax.markup_command Thy_Output.Markup |
84 Outer_Syntax.markup_command Thy_Output.Markup |
85 ("subsect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)" |
85 ("subsect", Keyword.tag_proof Keyword.prf_heading3) "formal comment (proof)" |
86 (Parse.doc_source >> Isar_Cmd.proof_markup); |
86 (Parse.doc_source >> Isar_Cmd.proof_markup); |
87 |
87 |
88 val _ = |
88 val _ = |
89 Outer_Syntax.markup_command Thy_Output.Markup |
89 Outer_Syntax.markup_command Thy_Output.Markup |
90 ("subsubsect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)" |
90 ("subsubsect", Keyword.tag_proof Keyword.prf_heading4) "formal comment (proof)" |
91 (Parse.doc_source >> Isar_Cmd.proof_markup); |
91 (Parse.doc_source >> Isar_Cmd.proof_markup); |
92 |
92 |
93 val _ = |
93 val _ = |
94 Outer_Syntax.markup_command Thy_Output.MarkupEnv |
94 Outer_Syntax.markup_command Thy_Output.MarkupEnv |
95 ("txt", Keyword.tag_proof Keyword.prf_decl) "formal comment (proof)" |
95 ("txt", Keyword.tag_proof Keyword.prf_decl) "formal comment (proof)" |