src/Pure/Thy/thy_output.ML
changeset 61461 77c9643a6353
parent 61459 5f2ddeb15c06
child 61462 e16649b70107
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sat Oct 17 19:32:01 2015 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Oct 17 19:47:34 2015 +0200
     1.3 @@ -192,9 +192,12 @@
     1.4      val output_antiquote = eval_antiquote state #> Symbol.explode #> Latex.output_ctrl_symbols;
     1.5      val output_antiquotes = map output_antiquote #> implode;
     1.6  
     1.7 +    fun output_line line =
     1.8 +      (if Markdown.line_is_item line then "\\item " else "") ^
     1.9 +        output_antiquotes (Markdown.line_content line);
    1.10 +
    1.11      fun output_blocks blocks = space_implode "\n\n" (map output_block blocks)
    1.12 -    and output_block (Markdown.Paragraph lines) =
    1.13 -          cat_lines (map (output_antiquotes o Markdown.line_source) lines)
    1.14 +    and output_block (Markdown.Paragraph lines) = cat_lines (map output_line lines)
    1.15        | output_block (Markdown.List {kind, body, ...}) =
    1.16            let val env = Markdown.print_kind kind in
    1.17              "%\n\\begin{" ^ env ^ "}%\n" ^