--- a/src/Pure/Thy/markdown.ML Sun Oct 23 12:34:39 2016 +0200
+++ b/src/Pure/Thy/markdown.ML Sun Oct 23 12:35:48 2016 +0200
@@ -28,7 +28,7 @@
val line_content: line -> Antiquote.text_antiquote list
val make_line: Antiquote.text_antiquote list -> line
val empty_line: line
- datatype block = Paragraph of line list | List of {indent: int, kind: kind, body: block list}
+ datatype block = Par of line list | List of {indent: int, kind: kind, body: block list}
val read_lines: line list -> block list
val read_antiquotes: Antiquote.text_antiquote list -> block list
val read_source: Input.source -> block list
@@ -124,17 +124,16 @@
(* document blocks *)
-datatype block =
- Paragraph of line list | List of {indent: int, kind: kind, body: block list};
+datatype block = Par of line list | List of {indent: int, kind: kind, body: block list};
-fun block_lines (Paragraph lines) = lines
+fun block_lines (Par lines) = lines
| block_lines (List {body, ...}) = maps block_lines body;
-fun block_range (Paragraph lines) = Antiquote.range (maps line_content lines)
+fun block_range (Par lines) = Antiquote.range (maps line_content lines)
| block_range (List {body, ...}) = Antiquote.range (maps line_source (maps block_lines body));
fun block_indent (List {indent, ...}) = indent
- | block_indent (Paragraph (Line {indent, ...} :: _)) = indent
+ | block_indent (Par (Line {indent, ...} :: _)) = indent
| block_indent _ = 0;
fun block_list indent0 kind0 (List {indent, kind, body}) =
@@ -167,7 +166,7 @@
Scan.one (fn line => line <> eof_line) -- Scan.many plain_line >> (fn (line, lines) =>
let
val Line {indent, item, ...} = line;
- val block = Paragraph (line :: lines);
+ val block = Par (line :: lines);
in (indent, item, [block]) end);
val parse_document =
@@ -199,7 +198,7 @@
fun block_reports depth block =
(case block of
- Paragraph lines =>
+ Par lines =>
cons (#1 (block_range block), Markup.markdown_paragraph) #>
fold (line_reports depth) lines
| List {kind, body, ...} =>
--- a/src/Pure/Thy/thy_output.ML Sun Oct 23 12:34:39 2016 +0200
+++ b/src/Pure/Thy/thy_output.ML Sun Oct 23 12:35:48 2016 +0200
@@ -215,7 +215,7 @@
output_antiquotes (Markdown.line_content line);
fun output_blocks blocks = space_implode "\n\n" (map output_block blocks)
- and output_block (Markdown.Paragraph lines) = cat_lines (map output_line lines)
+ and output_block (Markdown.Par lines) = cat_lines (map output_line lines)
| output_block (Markdown.List {kind, body, ...}) =
Latex.environment (Markdown.print_kind kind) (output_blocks body);
in