PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);

--- a/src/Pure/PIDE/markup.ML	Tue Jan 02 15:38:22 2018 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Jan 02 19:52:17 2018 +0100
@@ -122,6 +122,7 @@
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
   val markdown_paragraphN: string val markdown_paragraph: T
+  val markdown_itemN: string val markdown_item: T
   val markdown_listN: string val markdown_list: string -> T
   val markdown_bulletN: string val markdown_bullet: int -> T
   val inputN: string val input: bool -> Properties.T -> T
@@ -473,6 +474,7 @@
 (* Markdown document structure *)
 
 val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph";
+val (markdown_itemN, markdown_item) = markup_elem "markdown_item";
 val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN;
 val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth";
 

--- a/src/Pure/PIDE/markup.scala	Tue Jan 02 15:38:22 2018 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Jan 02 19:52:17 2018 +0100
@@ -296,6 +296,7 @@
   /* Markdown document structure */
 
   val MARKDOWN_PARAGRAPH = "markdown_paragraph"
+  val MARKDOWN_ITEM = "markdown_item"
   val Markdown_List = new Markup_String("markdown_list", "kind")
   val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
 

--- a/src/Pure/PIDE/rendering.scala	Tue Jan 02 15:38:22 2018 +0100
+++ b/src/Pure/PIDE/rendering.scala	Tue Jan 02 19:52:17 2018 +0100
@@ -197,7 +197,8 @@
     Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
       Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
       Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
-      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
+      Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++
+      Markup.Elements(tooltip_descriptions.keySet)
 
   val tooltip_message_elements =
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
@@ -591,6 +592,8 @@
 
           case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
             Some(info + (r0, true, XML.Text("Markdown: paragraph")))
+          case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), _))) =>
+            Some(info + (r0, true, XML.Text("Markdown: item")))
           case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) =>
             Some(info + (r0, true, XML.Text("Markdown: " + kind)))
 

--- 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

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Jan 02 15:38:22 2018 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Jan 02 19:52:17 2018 +0100
@@ -120,7 +120,7 @@
       Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
       Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
       Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
-      Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name)
+      Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name)
 
   private val hyperlink_elements =
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.POSITION,