# HG changeset patch
# User wenzelm
# Date 1445104054 -7200
# Node ID 77c9643a6353abf4c624e3f3fb08a3f244536bc2
# Parent  732028edfbc7b67d41a4c64bddccc03ce8d1c326
more explicit output of list items;

diff -r 732028edfbc7 -r 77c9643a6353 NEWS
--- a/NEWS	Sat Oct 17 19:32:01 2015 +0200
+++ b/NEWS	Sat Oct 17 19:47:34 2015 +0200
@@ -64,9 +64,12 @@
   \<^medskip>   \medskip
   \<^bigskip>   \bigskip
 
-  \<^item>  \item  (itemize)
-  \<^enum>  \item  (enumerate)
-  \<^descr>  \item  (description)
+* Paragraphs and nested lists may be specified similarly to Markdown,
+with control symbols to indicate list items as follows:
+
+  \<^item>  itemize
+  \<^enum>  enumerate
+  \<^descr>  description
 
 
 *** Isar ***
diff -r 732028edfbc7 -r 77c9643a6353 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Sat Oct 17 19:32:01 2015 +0200
+++ b/lib/texinputs/isabelle.sty	Sat Oct 17 19:47:34 2015 +0200
@@ -43,9 +43,6 @@
 \def\isactrlsmallskip{\smallskip}
 \def\isactrlmedskip{\medskip}
 \def\isactrlbigskip{\bigskip}
-\def\isactrlitem{\item}
-\def\isactrlenum{\item}
-\def\isactrldescr{\item}
 
 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
diff -r 732028edfbc7 -r 77c9643a6353 src/Pure/Thy/markdown.ML
--- a/src/Pure/Thy/markdown.ML	Sat Oct 17 19:32:01 2015 +0200
+++ b/src/Pure/Thy/markdown.ML	Sat Oct 17 19:47:34 2015 +0200
@@ -24,6 +24,7 @@
   val print_kind: kind -> string
   type line
   val line_source: line -> Antiquote.text_antiquote list
+  val line_is_item: line -> bool
   val line_content: line -> Antiquote.text_antiquote list
   val make_line: Antiquote.text_antiquote list -> line
   val empty_line: line
@@ -63,6 +64,7 @@
 
 fun line_source (Line {source, ...}) = source;
 fun line_is_empty (Line {is_empty, ...}) = is_empty;
+fun line_is_item (Line {item, ...}) = is_some item;
 fun line_content (Line {content, ...}) = content;
 
 
diff -r 732028edfbc7 -r 77c9643a6353 src/Pure/Thy/thy_output.ML
--- 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" ^