src/Pure/Isar/isar_syn.ML
changeset 9552 e3981c1f769d
parent 9465 b285b91cd2b2
child 9589 95a66548c883
equal deleted inserted replaced
9551:f4bfb69ae94e 9552:e3981c1f769d
    58 val text_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "text_raw"
    58 val text_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "text_raw"
    59   "raw document preparation text" K.thy_decl
    59   "raw document preparation text" K.thy_decl
    60   (P.comment >> (Toplevel.theory o IsarThy.add_text_raw));
    60   (P.comment >> (Toplevel.theory o IsarThy.add_text_raw));
    61 
    61 
    62 
    62 
    63 val sectP = OuterSyntax.markup_command IsarOutput.Markup "sect" "formal comment (proof)" K.prf_decl
    63 val sectP = OuterSyntax.markup_command IsarOutput.Markup "sect" "formal comment (proof)"
    64   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));
    64   K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));
    65 
    65 
    66 val subsectP = OuterSyntax.markup_command IsarOutput.Markup "subsect" "formal comment (proof)"
    66 val subsectP = OuterSyntax.markup_command IsarOutput.Markup "subsect" "formal comment (proof)"
    67   K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
    67   K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
    68 
    68 
    69 val subsubsectP = OuterSyntax.markup_command IsarOutput.Markup "subsubsect"
    69 val subsubsectP = OuterSyntax.markup_command IsarOutput.Markup "subsubsect"
    70   "formal comment (proof)" K.prf_decl
    70   "formal comment (proof)" K.prf_heading
    71   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect)));
    71   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect)));
    72 
    72 
    73 val txtP = OuterSyntax.markup_command IsarOutput.MarkupEnv "txt" "formal comment (proof)"
    73 val txtP = OuterSyntax.markup_command IsarOutput.MarkupEnv "txt" "formal comment (proof)"
    74   K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
    74   K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
    75 
    75