# HG changeset patch
# User wenzelm
# Date 1444905782 -7200
# Node ID 31aadb15eda5a743cdb66eefd2c21512c8e00c33
# Parent  1fcdfc1a7e503a2f7be91aa684850a14fe471ce8
more document structure;
tuned signature;

diff -r 1fcdfc1a7e50 -r 31aadb15eda5 src/Pure/Thy/markdown.ML
--- a/src/Pure/Thy/markdown.ML	Wed Oct 14 21:18:37 2015 +0200
+++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 12:43:02 2015 +0200
@@ -7,32 +7,38 @@
 signature MARKDOWN =
 sig
   datatype kind = Itemize | Enumerate | Description
+  type marker = {indent: int, kind: kind}
   type line
   val line_content: line -> Antiquote.text_antiquote list
-  datatype block = Paragraph of line list | List of kind * block list
-  val read_document: Input.source -> block list
+  val make_line: Antiquote.text_antiquote list -> line
+  val empty_line: line
+  datatype block = Paragraph of line list | List of marker * block list
+  val read_lines: line list -> block list
+  val read: Input.source -> block list
 end;
 
 structure Markdown: MARKDOWN =
 struct
 
-(* document structure *)
+(* document lines *)
 
 datatype kind = Itemize | Enumerate | Description;
-type marker = {indent: int, kind: kind, pos: Position.T};
+type marker = {indent: int, kind: kind};
 
 datatype line =
   Line of
    {content: Antiquote.text_antiquote list,
     is_empty: bool,
-    marker: marker option};
+    marker: (marker * Position.T) option};
+
+val eof_line =
+  Line {content = [Antiquote.Text [(Symbol.eof, Position.none)]],
+    is_empty = false, marker = NONE};
 
 fun line_content (Line {content, ...}) = content;
 fun line_is_empty (Line {is_empty, ...}) = is_empty;
 fun line_marker (Line {marker, ...}) = marker;
 
-datatype block = Paragraph of line list | List of kind * block list;
-
 
 (* make line *)
 
@@ -52,14 +58,12 @@
 
 val scan_marker =
   Scan.many is_space --
-    (Symbol_Pos.$$ "\<^item>" >> K Itemize ||
-     Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
-     Symbol_Pos.$$ "\<^descr>" >> K Description)
-    -- Symbol_Pos.scan_pos
-    >> (fn ((a, b), c) => ({indent = length a, kind = b, pos = c}: marker));
+  (Symbol_Pos.$$ "\<^item>" >> K Itemize ||
+   Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
+   Symbol_Pos.$$ "\<^descr>" >> K Description) >> (fn (a, b) => {indent = length a, kind = b});
 
 fun read_marker (Antiquote.Text ss :: _) =
-      #1 (Scan.finite Symbol_Pos.stopper (Scan.option scan_marker) ss)
+      #1 (Scan.finite Symbol_Pos.stopper (Scan.option (scan_marker -- Symbol_Pos.scan_pos)) ss)
   | read_marker _ = NONE;
 
 in
@@ -70,21 +74,30 @@
     val marker = read_marker content;
   in Line {content = content, is_empty = is_empty content, marker = marker} end;
 
+val empty_line = make_line [];
+
 end;
 
 
+(* document blocks *)
+
+datatype block = Paragraph of line list | List of marker * block list;
+
+fun add_span (opt_marker, body) document =
+  (case (opt_marker, document) of
+    (SOME marker, List (list_marker, list_body) :: rest) =>
+      if marker = list_marker then List (list_marker, body @ list_body) :: rest
+      else List (marker, body) :: document
+  | (SOME marker, _) => List (marker, body) :: document
+  | (NONE, _) => body @ document);
+
+
 (* read document *)
 
 local
 
-val eof =
-  Line {content = [Antiquote.Text [(Symbol.eof, Position.none)]],
-    is_empty = false, marker = NONE};
-
-val stopper = Scan.stopper (K eof) (fn line => line = eof);
-
 fun plain_line line =
-  not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof;
+  not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof_line;
 
 val parse_paragraph = Scan.many1 plain_line >> Paragraph;
 
@@ -92,20 +105,22 @@
   parse_paragraph >> (fn par => (NONE, [par])) ||
   Scan.one (is_some o line_marker) -- Scan.many plain_line --
     Scan.repeat (Scan.one line_is_empty |-- parse_paragraph) >>
-      (fn ((line, lines), pars) => ((line_marker line), Paragraph (line :: lines) :: pars));
+      (fn ((line, lines), pars) =>
+        (Option.map #1 (line_marker line), Paragraph (line :: lines) :: pars));
 
 val parse_document =
-  parse_span ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_span) >> maps snd;
-
-val parse_documents =
-  Scan.repeat (Scan.many line_is_empty |-- parse_document) --| Scan.many line_is_empty >> flat;
+  parse_span ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_span)
+    >> (fn spans => fold_rev add_span spans []);
 
 in
 
-val read_document =
-  Antiquote.read #> Antiquote.split_lines #> map make_line #>
-  Scan.read stopper parse_documents #> the_default [];
+val read_lines =
+  Scan.read (Scan.stopper (K eof_line) (fn line => line = eof_line))
+    (Scan.repeat (Scan.many line_is_empty |-- parse_document) --| Scan.many line_is_empty) #>
+  the_default [] #> flat;
 
 end;
 
+val read = Antiquote.read #> Antiquote.split_lines #> map make_line #> read_lines;
+
 end;