56 (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection)); |
56 (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection)); |
57 |
57 |
58 val textP = OuterSyntax.markup_command "text" "formal comment (theory)" K.thy_decl |
58 val textP = OuterSyntax.markup_command "text" "formal comment (theory)" K.thy_decl |
59 (P.comment >> (Toplevel.theory o IsarThy.add_text)); |
59 (P.comment >> (Toplevel.theory o IsarThy.add_text)); |
60 |
60 |
61 val verbatimP = OuterSyntax.verbatim_command "verbatim" "verbatim document preparation text" |
61 val text_rawP = OuterSyntax.verbatim_command "text_raw" "raw document preparation text" |
62 K.thy_decl (P.comment >> (Toplevel.theory o IsarThy.add_verbatim)); |
62 K.thy_decl (P.comment >> (Toplevel.theory o IsarThy.add_text_raw)); |
63 |
63 |
64 |
64 |
65 val sectP = OuterSyntax.markup_command "sect" "formal comment (proof)" K.prf_decl |
65 val sectP = OuterSyntax.markup_command "sect" "formal comment (proof)" K.prf_decl |
66 (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect))); |
66 (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect))); |
67 |
67 |
72 (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect))); |
72 (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect))); |
73 |
73 |
74 val txtP = OuterSyntax.markup_command "txt" "formal comment (proof)" K.prf_decl |
74 val txtP = OuterSyntax.markup_command "txt" "formal comment (proof)" K.prf_decl |
75 (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt))); |
75 (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt))); |
76 |
76 |
77 val verbP = OuterSyntax.verbatim_command "verb" "verbatim document preparation text (proof)" |
77 val txt_rawP = OuterSyntax.verbatim_command "txt_raw" "raw document preparation text (proof)" |
78 K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_verb))); |
78 K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt_raw))); |
79 |
79 |
80 |
80 |
81 |
81 |
82 (** theory sections **) |
82 (** theory sections **) |
83 |
83 |
605 val parsers = [ |
605 val parsers = [ |
606 (*theory structure*) |
606 (*theory structure*) |
607 theoryP, end_excursionP, kill_excursionP, contextP, |
607 theoryP, end_excursionP, kill_excursionP, contextP, |
608 (*markup commands*) |
608 (*markup commands*) |
609 headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP, |
609 headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP, |
610 verbatimP, sectP, subsectP, subsubsectP, txtP, verbP, |
610 text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP, |
611 (*theory sections*) |
611 (*theory sections*) |
612 classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP, |
612 classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP, |
613 aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP, |
613 aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP, |
614 constdefsP, theoremsP, lemmasP, globalP, localP, useP, mlP, |
614 constdefsP, theoremsP, lemmasP, globalP, localP, useP, mlP, |
615 ml_setupP, setupP, parse_ast_translationP, parse_translationP, |
615 ml_setupP, setupP, parse_ast_translationP, parse_translationP, |