report Markdown document structure;

--- a/src/Pure/PIDE/markup.ML	Thu Oct 15 13:48:47 2015 +0200
+++ b/src/Pure/PIDE/markup.ML	Thu Oct 15 15:06:03 2015 +0200
@@ -117,6 +117,9 @@
   val document_antiquotation_optionN: string
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
+  val markdown_paragraphN: string val markdown_paragraph: T
+  val markdown_listN: string val markdown_list: string -> T
+  val markdown_itemN: string val markdown_item: int -> T
   val inputN: string val input: bool -> Properties.T -> T
   val command_keywordN: string val command_keyword: T
   val commandN: string val command: T
@@ -465,6 +468,13 @@
 val (text_foldN, text_fold) = markup_elem "text_fold";
 
 
+(* Markdown document structure *)
+
+val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph";
+val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN;
+val (markdown_itemN, markdown_item) = markup_int "markdown_item" "depth";
+
+
 (* formal input *)
 
 val inputN = "input";

--- a/src/Pure/PIDE/markup.scala	Thu Oct 15 13:48:47 2015 +0200
+++ b/src/Pure/PIDE/markup.scala	Thu Oct 15 15:06:03 2015 +0200
@@ -243,6 +243,13 @@
   val TEXT_FOLD = "text_fold"
 
 
+  /* Markdown document structure */
+
+  val MARKDOWN_PARAGRAPH = "markdown_paragraph"
+  val Markdown_List = new Markup_String("markdown_list", "kind")
+  val Markdown_Item = new Markup_Int("markdown_item", "depth")
+
+
   /* ML */
 
   val ML_KEYWORD1 = "ML_keyword1"

--- a/src/Pure/Thy/markdown.ML	Thu Oct 15 13:48:47 2015 +0200
+++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 15:06:03 2015 +0200
@@ -20,6 +20,7 @@
 signature MARKDOWN =
 sig
   datatype kind = Itemize | Enumerate | Description
+  val print_kind: kind -> string
   type marker = {indent: int, kind: kind}
   type line
   val line_content: line -> Antiquote.text_antiquote list
@@ -28,6 +29,7 @@
   datatype block = Paragraph of line list | List of marker * block list
   val read_lines: line list -> block list
   val read: Input.source -> block list
+  val reports: block list -> Position.report list
 end;
 
 structure Markdown: MARKDOWN =
@@ -36,6 +38,11 @@
 (* document lines *)
 
 datatype kind = Itemize | Enumerate | Description;
+
+fun print_kind Itemize = "itemize"
+  | print_kind Enumerate = "enumerate"
+  | print_kind Description = "description";
+
 type marker = {indent: int, kind: kind};
 
 datatype line =
@@ -70,13 +77,14 @@
 val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
 
 val scan_marker =
-  Scan.many is_space --
+  Scan.many is_space -- Symbol_Pos.scan_pos --
   (Symbol_Pos.$$ "\<^item>" >> K Itemize ||
    Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
-   Symbol_Pos.$$ "\<^descr>" >> K Description) >> (fn (a, b) => {indent = length a, kind = b});
+   Symbol_Pos.$$ "\<^descr>" >> K Description)
+  >> (fn ((spaces, pos), kind) => ({indent = length spaces, kind = kind}, pos));
 
 fun read_marker (Antiquote.Text ss :: _) =
-      #1 (Scan.finite Symbol_Pos.stopper (Scan.option (scan_marker -- Symbol_Pos.scan_pos)) ss)
+      #1 (Scan.finite Symbol_Pos.stopper (Scan.option scan_marker) ss)
   | read_marker _ = NONE;
 
 in
@@ -140,4 +148,22 @@
 
 val read = Antiquote.read #> Antiquote.split_lines #> map make_line #> read_lines;
 
+
+(* PIDE reports *)
+
+local
+
+fun line_reports depth (Line {marker = SOME (_, pos), ...}) =
+      Position.is_reported pos ? cons (pos, Markup.markdown_item depth)
+  | line_reports _ _ = I;
+
+fun block_reports depth (Paragraph lines) = fold (line_reports depth) lines
+  | block_reports depth (List (_, body)) = fold (block_reports (depth + 1)) body;
+
+in
+
+fun reports blocks = fold (block_reports 0) blocks [];
+
 end;
+
+end;

--- a/src/Tools/jEdit/etc/options	Thu Oct 15 13:48:47 2015 +0200
+++ b/src/Tools/jEdit/etc/options	Thu Oct 15 15:06:03 2015 +0200
@@ -133,6 +133,11 @@
 option inner_comment_color : string = "CC0000FF"
 option dynamic_color : string = "7BA428FF"
 
+option markdown_item_color1 : string = "DAFEDAFF"
+option markdown_item_color2 : string = "FFF0CCFF"
+option markdown_item_color3 : string = "E7E7FFFF"
+option markdown_item_color4 : string = "FFE0F0FF"
+
 
 section "Icons"
 

--- a/src/Tools/jEdit/src/rendering.scala	Thu Oct 15 13:48:47 2015 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Oct 15 15:06:03 2015 +0200
@@ -204,7 +204,7 @@
       Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
       Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
       Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
-      Markup.BAD + Markup.INTENSIFY ++ active_elements
+      Markup.BAD + Markup.INTENSIFY + Markup.Markdown_Item.name ++ active_elements
 
   private val foreground_elements =
     Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
@@ -282,6 +282,11 @@
   val inner_comment_color = color_value("inner_comment_color")
   val dynamic_color = color_value("dynamic_color")
 
+  val markdown_item_color1 = color_value("markdown_item_color1")
+  val markdown_item_color2 = color_value("markdown_item_color2")
+  val markdown_item_color3 = color_value("markdown_item_color3")
+  val markdown_item_color4 = color_value("markdown_item_color4")
+
 
   /* completion */
 
@@ -679,6 +684,15 @@
                   Some((Nil, Some(bad_color)))
                 case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
                   Some((Nil, Some(intensify_color)))
+                case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>
+                  val color =
+                    depth match {
+                      case 1 => markdown_item_color1
+                      case 2 => markdown_item_color2
+                      case 3 => markdown_item_color3
+                      case _ => markdown_item_color4
+                    }
+                  Some((Nil, Some(color)))
                 case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
                   command_states.collectFirst(
                     { case st if st.results.defined(serial) => st.results.get(serial).get }) match