src/Pure/Thy/markdown.ML
changeset 61460 732028edfbc7
parent 61459 5f2ddeb15c06
child 61461 77c9643a6353
     1.1 --- a/src/Pure/Thy/markdown.ML	Sat Oct 17 19:26:34 2015 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Sat Oct 17 19:32:01 2015 +0200
     1.3 @@ -63,9 +63,6 @@
     1.4  
     1.5  fun line_source (Line {source, ...}) = source;
     1.6  fun line_is_empty (Line {is_empty, ...}) = is_empty;
     1.7 -fun line_indent (Line {indent, ...}) = indent;
     1.8 -fun line_item (Line {item, ...}) = item;
     1.9 -fun line_item_pos (Line {item_pos, ...}) = item_pos;
    1.10  fun line_content (Line {content, ...}) = content;
    1.11  
    1.12  
    1.13 @@ -127,7 +124,7 @@
    1.14    | block_range (List {body, ...}) = Antiquote.range (maps line_source (maps block_lines body));
    1.15  
    1.16  fun block_indent (List {indent, ...}) = indent
    1.17 -  | block_indent (Paragraph (line :: _)) = line_indent line
    1.18 +  | block_indent (Paragraph (Line {indent, ...} :: _)) = indent
    1.19    | block_indent _ = 0;
    1.20  
    1.21  fun block_list indent0 kind0 (List {indent, kind, body}) =
    1.22 @@ -153,13 +150,15 @@
    1.23    | (SOME kind, []) => [List {indent = indent, kind = kind, body = rev rev_body}]
    1.24    | (NONE, _) => fold cons rev_body document);
    1.25  
    1.26 -fun plain_line line =
    1.27 -  not (line_is_empty line) andalso is_none (line_item line) andalso line <> eof_line;
    1.28 +fun plain_line (line as Line {is_empty, item, ...}) =
    1.29 +  not is_empty andalso is_none item andalso line <> eof_line;
    1.30  
    1.31  val parse_paragraph =
    1.32    Scan.one (fn line => line <> eof_line) -- Scan.many plain_line >> (fn (line, lines) =>
    1.33 -    let val block = Paragraph (line :: lines)
    1.34 -    in (line_indent line, line_item line, [block]) end);
    1.35 +    let
    1.36 +      val Line {indent, item, ...} = line;
    1.37 +      val block = Paragraph (line :: lines);
    1.38 +    in (indent, item, [block]) end);
    1.39  
    1.40  val parse_document =
    1.41    parse_paragraph ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_paragraph)
    1.42 @@ -185,9 +184,8 @@
    1.43  
    1.44  local
    1.45  
    1.46 -fun line_reports depth line =
    1.47 -  cons (line_item_pos line, Markup.markdown_item depth) #>
    1.48 -  append (text_reports (line_content line));
    1.49 +fun line_reports depth (Line {item_pos, content, ...}) =
    1.50 +  cons (item_pos, Markup.markdown_item depth) #> append (text_reports content);
    1.51  
    1.52  fun block_reports depth block =
    1.53    (case block of