# HG changeset patch
# User wenzelm
# Date 1444919834 -7200
# Node ID fa665e3df0ca119836ed2779417a3fb4543838fc
# Parent  7f530057bc3cb56bf50baf33dd2c27fa5df1391b
tuned;

diff -r 7f530057bc3c -r fa665e3df0ca src/Pure/Thy/markdown.ML
--- a/src/Pure/Thy/markdown.ML	Thu Oct 15 16:30:54 2015 +0200
+++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 16:37:14 2015 +0200
@@ -112,6 +112,13 @@
 fun block_lines (Paragraph lines) = lines
   | block_lines (List (_, blocks)) = maps block_lines blocks;
 
+fun block_range (Paragraph lines) = Antiquote.range (maps line_content lines)
+  | block_range (List (_, blocks)) = Antiquote.range (maps line_source (maps block_lines blocks));
+
+
+(* read document *)
+
+local
 
 fun add_span (opt_marker, body) document =
   (case (opt_marker, document) of
@@ -125,11 +132,6 @@
   | (SOME marker, _) => List (marker, body) :: document
   | (NONE, _) => body @ document);
 
-
-(* read document *)
-
-local
-
 fun plain_line line =
   not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof_line;
 
@@ -166,13 +168,14 @@
       cons (pos, Markup.markdown_item depth)
   | line_reports _ _ = I;
 
-fun block_reports depth (Paragraph lines) =
-      cons (#1 (Antiquote.range (maps line_content lines)), Markup.markdown_paragraph) #>
+fun block_reports depth block =
+  (case block of
+    Paragraph lines =>
+      cons (#1 (block_range block), Markup.markdown_paragraph) #>
       fold (line_reports depth) lines
-  | block_reports depth (List ({kind, ...}, body)) =
-      cons (#1 (Antiquote.range (maps line_source (maps block_lines body))),
-        Markup.markdown_list (print_kind kind)) #>
-      fold (block_reports (depth + 1)) body;
+  | List ({kind, ...}, body) =>
+      cons (#1 (block_range block), Markup.markdown_list (print_kind kind)) #>
+      fold (block_reports (depth + 1)) body);
 
 in