tuned;
authorwenzelm
Thu Oct 15 16:37:14 2015 +0200 (2015-10-15)
changeset 61452fa665e3df0ca
parent 61451 7f530057bc3c
child 61453 3a3e3527445e
tuned;
src/Pure/Thy/markdown.ML
     1.1 --- a/src/Pure/Thy/markdown.ML	Thu Oct 15 16:30:54 2015 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 16:37:14 2015 +0200
     1.3 @@ -112,6 +112,13 @@
     1.4  fun block_lines (Paragraph lines) = lines
     1.5    | block_lines (List (_, blocks)) = maps block_lines blocks;
     1.6  
     1.7 +fun block_range (Paragraph lines) = Antiquote.range (maps line_content lines)
     1.8 +  | block_range (List (_, blocks)) = Antiquote.range (maps line_source (maps block_lines blocks));
     1.9 +
    1.10 +
    1.11 +(* read document *)
    1.12 +
    1.13 +local
    1.14  
    1.15  fun add_span (opt_marker, body) document =
    1.16    (case (opt_marker, document) of
    1.17 @@ -125,11 +132,6 @@
    1.18    | (SOME marker, _) => List (marker, body) :: document
    1.19    | (NONE, _) => body @ document);
    1.20  
    1.21 -
    1.22 -(* read document *)
    1.23 -
    1.24 -local
    1.25 -
    1.26  fun plain_line line =
    1.27    not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof_line;
    1.28  
    1.29 @@ -166,13 +168,14 @@
    1.30        cons (pos, Markup.markdown_item depth)
    1.31    | line_reports _ _ = I;
    1.32  
    1.33 -fun block_reports depth (Paragraph lines) =
    1.34 -      cons (#1 (Antiquote.range (maps line_content lines)), Markup.markdown_paragraph) #>
    1.35 +fun block_reports depth block =
    1.36 +  (case block of
    1.37 +    Paragraph lines =>
    1.38 +      cons (#1 (block_range block), Markup.markdown_paragraph) #>
    1.39        fold (line_reports depth) lines
    1.40 -  | block_reports depth (List ({kind, ...}, body)) =
    1.41 -      cons (#1 (Antiquote.range (maps line_source (maps block_lines body))),
    1.42 -        Markup.markdown_list (print_kind kind)) #>
    1.43 -      fold (block_reports (depth + 1)) body;
    1.44 +  | List ({kind, ...}, body) =>
    1.45 +      cons (#1 (block_range block), Markup.markdown_list (print_kind kind)) #>
    1.46 +      fold (block_reports (depth + 1)) body);
    1.47  
    1.48  in
    1.49