# HG changeset patch
# User wenzelm
# Date 1477218948 -7200
# Node ID e10fa8afc96c728080e0dd5c974d38300a149756
# Parent  ebbe7cf0c2b80b2b24564c093d297cde82064e3b
tuned signature: avoid conflict with "paragraph" as section heading;

diff -r ebbe7cf0c2b8 -r e10fa8afc96c src/Pure/Thy/markdown.ML
--- 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, ...} =>
diff -r ebbe7cf0c2b8 -r e10fa8afc96c src/Pure/Thy/thy_output.ML
--- 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