src/Pure/Thy/markdown.ML
changeset 64357 e10fa8afc96c
parent 62804 7b9c5416f30e
child 67322 734a4e44b159
     1.1 --- a/src/Pure/Thy/markdown.ML	Sun Oct 23 12:34:39 2016 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Sun Oct 23 12:35:48 2016 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4    val line_content: line -> Antiquote.text_antiquote list
     1.5    val make_line: Antiquote.text_antiquote list -> line
     1.6    val empty_line: line
     1.7 -  datatype block = Paragraph of line list | List of {indent: int, kind: kind, body: block list}
     1.8 +  datatype block = Par of line list | List of {indent: int, kind: kind, body: block list}
     1.9    val read_lines: line list -> block list
    1.10    val read_antiquotes: Antiquote.text_antiquote list -> block list
    1.11    val read_source: Input.source -> block list
    1.12 @@ -124,17 +124,16 @@
    1.13  
    1.14  (* document blocks *)
    1.15  
    1.16 -datatype block =
    1.17 -  Paragraph of line list | List of {indent: int, kind: kind, body: block list};
    1.18 +datatype block = Par of line list | List of {indent: int, kind: kind, body: block list};
    1.19  
    1.20 -fun block_lines (Paragraph lines) = lines
    1.21 +fun block_lines (Par lines) = lines
    1.22    | block_lines (List {body, ...}) = maps block_lines body;
    1.23  
    1.24 -fun block_range (Paragraph lines) = Antiquote.range (maps line_content lines)
    1.25 +fun block_range (Par lines) = Antiquote.range (maps line_content lines)
    1.26    | block_range (List {body, ...}) = Antiquote.range (maps line_source (maps block_lines body));
    1.27  
    1.28  fun block_indent (List {indent, ...}) = indent
    1.29 -  | block_indent (Paragraph (Line {indent, ...} :: _)) = indent
    1.30 +  | block_indent (Par (Line {indent, ...} :: _)) = indent
    1.31    | block_indent _ = 0;
    1.32  
    1.33  fun block_list indent0 kind0 (List {indent, kind, body}) =
    1.34 @@ -167,7 +166,7 @@
    1.35    Scan.one (fn line => line <> eof_line) -- Scan.many plain_line >> (fn (line, lines) =>
    1.36      let
    1.37        val Line {indent, item, ...} = line;
    1.38 -      val block = Paragraph (line :: lines);
    1.39 +      val block = Par (line :: lines);
    1.40      in (indent, item, [block]) end);
    1.41  
    1.42  val parse_document =
    1.43 @@ -199,7 +198,7 @@
    1.44  
    1.45  fun block_reports depth block =
    1.46    (case block of
    1.47 -    Paragraph lines =>
    1.48 +    Par lines =>
    1.49        cons (#1 (block_range block), Markup.markdown_paragraph) #>
    1.50        fold (line_reports depth) lines
    1.51    | List {kind, body, ...} =>