src/Pure/Thy/markdown.ML
changeset 61450 239a04ec2d4c
parent 61449 4f31f79cf2d1
child 61451 7f530057bc3c
     1.1 --- a/src/Pure/Thy/markdown.ML	Thu Oct 15 15:06:03 2015 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 16:12:38 2015 +0200
     1.3 @@ -104,6 +104,10 @@
     1.4  
     1.5  datatype block = Paragraph of line list | List of marker * block list;
     1.6  
     1.7 +fun block_lines (Paragraph lines) = lines
     1.8 +  | block_lines (List (_, blocks)) = maps block_lines blocks;
     1.9 +
    1.10 +
    1.11  fun add_span (opt_marker, body) document =
    1.12    (case (opt_marker, document) of
    1.13      (SOME marker, (list as List (list_marker, list_body)) :: rest) =>
    1.14 @@ -154,15 +158,22 @@
    1.15  local
    1.16  
    1.17  fun line_reports depth (Line {marker = SOME (_, pos), ...}) =
    1.18 -      Position.is_reported pos ? cons (pos, Markup.markdown_item depth)
    1.19 +      cons (pos, Markup.markdown_item depth)
    1.20    | line_reports _ _ = I;
    1.21  
    1.22 -fun block_reports depth (Paragraph lines) = fold (line_reports depth) lines
    1.23 -  | block_reports depth (List (_, body)) = fold (block_reports (depth + 1)) body;
    1.24 +val lines_pos = #1 o Antiquote.range o maps line_content;
    1.25 +
    1.26 +fun block_reports depth (Paragraph lines) =
    1.27 +      cons (lines_pos lines, Markup.markdown_paragraph) #>
    1.28 +      fold (line_reports depth) lines
    1.29 +  | block_reports depth (List ({kind, ...}, body)) =
    1.30 +      cons (lines_pos (maps block_lines body), Markup.markdown_list (print_kind kind)) #>
    1.31 +      fold (block_reports (depth + 1)) body;
    1.32  
    1.33  in
    1.34  
    1.35 -fun reports blocks = fold (block_reports 0) blocks [];
    1.36 +fun reports blocks =
    1.37 +  filter (Position.is_reported o #1) (fold (block_reports 0) blocks []);
    1.38  
    1.39  end;
    1.40