src/Pure/Thy/markdown.ML

--- a/src/Pure/Thy/markdown.ML	Tue Jan 02 15:38:22 2018 +0100
+++ b/src/Pure/Thy/markdown.ML	Tue Jan 02 19:52:17 2018 +0100
@@ -129,6 +129,9 @@
 fun block_lines (Par lines) = lines
   | block_lines (List {body, ...}) = maps block_lines body;
 
+fun block_source (Par lines) = maps line_source lines
+  | block_source (List {body, ...}) = maps line_source (maps block_lines body);
+
 fun block_range (Par lines) = Antiquote.range (maps line_content lines)
   | block_range (List {body, ...}) = Antiquote.range (maps line_source (maps block_lines body));
 
@@ -142,6 +145,13 @@
 
 val is_list = fn List _ => true | _ => false;
 
+val is_item = fn Par (line :: _) => line_is_item line | _ => false;
+
+fun list_items [] = []
+  | list_items (item :: rest) =
+      let val (item_rest, rest') = take_prefix (not o is_item) rest;
+      in (item :: item_rest) :: list_items rest' end;
+
 
 (* read document *)
 
@@ -193,16 +203,23 @@
 
 local
 
+val block_pos = #1 o block_range;
+val item_pos = #1 o Antiquote.range o maps block_source;
+
 fun line_reports depth (Line {bullet_pos, content, ...}) =
   cons (bullet_pos, Markup.markdown_bullet depth) #> append (text_reports content);
 
+fun item_reports blocks =
+  cons (item_pos blocks, Markup.markdown_item);
+
 fun block_reports depth block =
   (case block of
     Par lines =>
-      cons (#1 (block_range block), Markup.markdown_paragraph) #>
+      cons (block_pos block, Markup.markdown_paragraph) #>
       fold (line_reports depth) lines
   | List {kind, body, ...} =>
-      cons (#1 (block_range block), Markup.markdown_list (print_kind kind)) #>
+      cons (block_pos block, Markup.markdown_list (print_kind kind)) #>
+      fold item_reports (list_items body) #>
       fold (block_reports (depth + 1)) body);
 
 in