more markup;

--- a/src/Pure/General/antiquote.ML	Thu Oct 15 15:06:03 2015 +0200
+++ b/src/Pure/General/antiquote.ML	Thu Oct 15 16:12:38 2015 +0200
@@ -9,6 +9,7 @@
   type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}
   datatype 'a antiquote = Text of 'a | Antiq of antiq
   type text_antiquote = Symbol_Pos.T list antiquote
+  val range: text_antiquote list -> Position.range
   val split_lines: text_antiquote list -> text_antiquote list list
   val antiq_reports: antiq -> Position.report list
   val antiquote_reports: ('a -> Position.report_text list) ->
@@ -28,6 +29,13 @@
 
 type text_antiquote = Symbol_Pos.T list antiquote;
 
+fun antiquote_range (Text ss) = Symbol_Pos.range ss
+  | antiquote_range (Antiq (_, {range, ...})) = range;
+
+fun range ants =
+  if null ants then Position.no_range
+  else Position.range (#1 (antiquote_range (hd ants))) (#2 (antiquote_range (List.last ants)));
+
 
 (* split lines *)
 

--- a/src/Pure/Thy/markdown.ML	Thu Oct 15 15:06:03 2015 +0200
+++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 16:12:38 2015 +0200
@@ -104,6 +104,10 @@
 
 datatype block = Paragraph of line list | List of marker * block list;
 
+fun block_lines (Paragraph lines) = lines
+  | block_lines (List (_, blocks)) = maps block_lines blocks;
+
+
 fun add_span (opt_marker, body) document =
   (case (opt_marker, document) of
     (SOME marker, (list as List (list_marker, list_body)) :: rest) =>
@@ -154,15 +158,22 @@
 local
 
 fun line_reports depth (Line {marker = SOME (_, pos), ...}) =
-      Position.is_reported pos ? cons (pos, Markup.markdown_item depth)
+      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;
+val lines_pos = #1 o Antiquote.range o maps line_content;
+
+fun block_reports depth (Paragraph lines) =
+      cons (lines_pos lines, Markup.markdown_paragraph) #>
+      fold (line_reports depth) lines
+  | block_reports depth (List ({kind, ...}, body)) =
+      cons (lines_pos (maps block_lines body), Markup.markdown_list (print_kind kind)) #>
+      fold (block_reports (depth + 1)) body;
 
 in
 
-fun reports blocks = fold (block_reports 0) blocks [];
+fun reports blocks =
+  filter (Position.is_reported o #1) (fold (block_reports 0) blocks []);
 
 end;
 

--- a/src/Tools/jEdit/src/rendering.scala	Thu Oct 15 15:06:03 2015 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Oct 15 16:12:38 2015 +0200
@@ -155,7 +155,8 @@
     Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
       Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
       Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
-      Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT)
+      Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
+      Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name)
 
   private val hyperlink_elements =
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION, Markup.URL)
@@ -182,7 +183,8 @@
 
   private val tooltip_elements =
     Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
-      Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.URL) ++
+      Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.URL,
+      Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++
     Markup.Elements(tooltip_descriptions.keySet)
 
   private val gutter_elements =
@@ -519,6 +521,7 @@
         {
           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
             Some(Text.Info(r, (t1 + t2, info)))
+
           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
             val kind1 = Word.implode(Word.explode('_', kind))
             val txt1 =
@@ -530,19 +533,24 @@
                 "\n" + t.message
               else ""
             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
+
           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
             val file = jedit_file(name)
             val text =
               if (name == file) "file " + quote(file)
               else "path " + quote(name) + "\nfile " + quote(file)
             Some(add(prev, r, (true, XML.Text(text))))
+
           case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
             Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
+
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
           if name == Markup.SORTING || name == Markup.TYPING =>
             Some(add(prev, r, (true, pretty_typing("::", body))))
+
           case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
             Some(add(prev, r, (false, pretty_typing("ML:", body))))
+
           case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
             val text =
               if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
@@ -550,6 +558,12 @@
             Some(add(prev, r, (true, XML.Text(text))))
           case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
             Some(add(prev, r, (true, XML.Text("language: " + language))))
+
+          case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
+            Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
+          case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
+            Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
+
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
             Rendering.tooltip_descriptions.get(name).
               map(descr => add(prev, r, (true, XML.Text(descr))))