src/Pure/pure_syn.ML
changeset 61457 3e21699bb83b
parent 61036 f6f2959bed67
child 61463 8e46cea6a45a
equal deleted inserted replaced
61456:b521b8b400f7 61457:3e21699bb83b
    17   Outer_Syntax.command ("header", @{here}) "theory header"
    17   Outer_Syntax.command ("header", @{here}) "theory header"
    18     (Parse.document_source >> Thy_Output.old_header_command);
    18     (Parse.document_source >> Thy_Output.old_header_command);
    19 
    19 
    20 val _ =
    20 val _ =
    21   Outer_Syntax.command ("chapter", @{here}) "chapter heading"
    21   Outer_Syntax.command ("chapter", @{here}) "chapter heading"
    22     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
    22     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
    23 
    23 
    24 val _ =
    24 val _ =
    25   Outer_Syntax.command ("section", @{here}) "section heading"
    25   Outer_Syntax.command ("section", @{here}) "section heading"
    26     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
    26     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
    27 
    27 
    28 val _ =
    28 val _ =
    29   Outer_Syntax.command ("subsection", @{here}) "subsection heading"
    29   Outer_Syntax.command ("subsection", @{here}) "subsection heading"
    30     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
    30     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
    31 
    31 
    32 val _ =
    32 val _ =
    33   Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading"
    33   Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading"
    34     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
    34     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
    35 
    35 
    36 val _ =
    36 val _ =
    37   Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
    37   Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
    38     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
    38     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
    39 
    39 
    40 val _ =
    40 val _ =
    41   Outer_Syntax.command ("txt", @{here}) "formal comment (secondary style)"
    41   Outer_Syntax.command ("txt", @{here}) "formal comment (secondary style)"
    42     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
    42     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
    43 
    43 
    44 val _ =
    44 val _ =
    45   Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text"
    45   Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text"
    46     (Parse.document_source >> (fn s => Toplevel.keep (fn _ => Thy_Output.report_text s)));
    46     (Parse.document_source >> (fn s => Thy_Output.document_command {markdown = true} (NONE, s)));
    47 
    47 
    48 val _ =
    48 val _ =
    49   Outer_Syntax.command ("theory", @{here}) "begin theory"
    49   Outer_Syntax.command ("theory", @{here}) "begin theory"
    50     (Thy_Header.args >>
    50     (Thy_Header.args >>
    51       (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
    51       (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));