equal
deleted
inserted
replaced
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 |