src/Pure/Thy/document_output.ML
changeset 74882 947bb3e09a88
parent 74838 4c8d9479f916
child 74887 56247fdb8bbb
equal deleted inserted replaced
74881:1e84ae3e886e 74882:947bb3e09a88
    90         output_antiquotes (Markdown.line_content line);
    90         output_antiquotes (Markdown.line_content line);
    91 
    91 
    92     fun output_block (Markdown.Par lines) =
    92     fun output_block (Markdown.Par lines) =
    93           separate (XML.Text "\n") (map (Latex.block o output_line) lines)
    93           separate (XML.Text "\n") (map (Latex.block o output_line) lines)
    94       | output_block (Markdown.List {kind, body, ...}) =
    94       | output_block (Markdown.List {kind, body, ...}) =
    95           Latex.environment_text (Markdown.print_kind kind) (output_blocks body)
    95           Latex.environment (Markdown.print_kind kind) (output_blocks body)
    96     and output_blocks blocks =
    96     and output_blocks blocks =
    97       separate (XML.Text "\n\n") (map (Latex.block o output_block) blocks);
    97       separate (XML.Text "\n\n") (map (Latex.block o output_block) blocks);
    98   in
    98   in
    99     if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then []
    99     if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then []
   100     else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
   100     else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms