39 |
39 |
40 |
40 |
41 (** markup commands **) |
41 (** markup commands **) |
42 |
42 |
43 val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag |
43 val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag |
44 (P.position P.text >> IsarCmd.add_header); |
44 (P.position P.text >> IsarCmd.header_markup); |
45 |
45 |
46 val _ = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading" |
46 val _ = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading" |
47 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_chapter); |
47 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.local_theory_markup); |
48 |
48 |
49 val _ = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading" |
49 val _ = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading" |
50 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_section); |
50 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.local_theory_markup); |
51 |
51 |
52 val _ = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading" |
52 val _ = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading" |
53 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsection); |
53 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.local_theory_markup); |
54 |
54 |
55 val _ = |
55 val _ = |
56 OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading" |
56 OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading" |
57 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsubsection); |
57 K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.local_theory_markup); |
58 |
58 |
59 val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)" |
59 val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)" |
60 K.thy_decl (P.opt_target -- P.position P.text >> IsarCmd.add_text); |
60 K.thy_decl (P.opt_target -- P.position P.text >> IsarCmd.local_theory_markup); |
61 |
61 |
62 val _ = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw" |
62 val _ = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw" |
63 "raw document preparation text" |
63 "raw document preparation text" |
64 K.thy_decl (P.position P.text >> IsarCmd.add_text_raw); |
64 K.thy_decl (P.opt_target -- P.position P.text >> IsarCmd.local_theory_markup); |
65 |
65 |
66 val _ = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)" |
66 val _ = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)" |
67 (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_sect); |
67 (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.proof_markup); |
68 |
68 |
69 val _ = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)" |
69 val _ = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)" |
70 (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_subsect); |
70 (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.proof_markup); |
71 |
71 |
72 val _ = OuterSyntax.markup_command ThyOutput.Markup "subsubsect" |
72 val _ = OuterSyntax.markup_command ThyOutput.Markup "subsubsect" |
73 "formal comment (proof)" (K.tag_proof K.prf_heading) |
73 "formal comment (proof)" (K.tag_proof K.prf_heading) |
74 (P.position P.text >> IsarCmd.add_subsubsect); |
74 (P.position P.text >> IsarCmd.proof_markup); |
75 |
75 |
76 val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)" |
76 val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)" |
77 (K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.add_txt); |
77 (K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.proof_markup); |
78 |
78 |
79 val _ = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw" |
79 val _ = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw" |
80 "raw document preparation text (proof)" (K.tag_proof K.prf_decl) |
80 "raw document preparation text (proof)" (K.tag_proof K.prf_decl) |
81 (P.position P.text >> IsarCmd.add_txt_raw); |
81 (P.position P.text >> IsarCmd.proof_markup); |
82 |
82 |
83 |
83 |
84 |
84 |
85 (** theory sections **) |
85 (** theory sections **) |
86 |
86 |