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