# HG changeset patch # User wenzelm # Date 1218653848 -7200 # Node ID be5372792b084a390dd42529b7d418b7e39afe70 # Parent 916038f77be6b6ebe0f7e47b07d078f6b80fc9ba simplified markup commands; diff -r 916038f77be6 -r be5372792b08 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Aug 13 20:57:26 2008 +0200 +++ b/src/Pure/Isar/isar_syn.ML Wed Aug 13 20:57:28 2008 +0200 @@ -41,44 +41,44 @@ (** markup commands **) val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag - (P.position P.text >> IsarCmd.add_header); + (P.position P.text >> IsarCmd.header_markup); val _ = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading" - K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_chapter); + K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.local_theory_markup); val _ = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading" - K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_section); + K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.local_theory_markup); val _ = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading" - K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsection); + K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.local_theory_markup); val _ = OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading" - K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsubsection); + K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.local_theory_markup); val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)" - K.thy_decl (P.opt_target -- P.position P.text >> IsarCmd.add_text); + K.thy_decl (P.opt_target -- P.position P.text >> IsarCmd.local_theory_markup); val _ = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw" "raw document preparation text" - K.thy_decl (P.position P.text >> IsarCmd.add_text_raw); + K.thy_decl (P.opt_target -- P.position P.text >> IsarCmd.local_theory_markup); val _ = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)" - (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_sect); + (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.proof_markup); val _ = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)" - (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_subsect); + (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.proof_markup); val _ = OuterSyntax.markup_command ThyOutput.Markup "subsubsect" "formal comment (proof)" (K.tag_proof K.prf_heading) - (P.position P.text >> IsarCmd.add_subsubsect); + (P.position P.text >> IsarCmd.proof_markup); val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)" - (K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.add_txt); + (K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.proof_markup); val _ = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw" "raw document preparation text (proof)" (K.tag_proof K.prf_decl) - (P.position P.text >> IsarCmd.add_txt_raw); + (P.position P.text >> IsarCmd.proof_markup);