src/Pure/Thy/markdown.ML

--- a/src/Pure/Thy/markdown.ML	Wed Oct 14 19:44:43 2015 +0200
+++ b/src/Pure/Thy/markdown.ML	Wed Oct 14 21:18:37 2015 +0200
@@ -9,7 +9,7 @@
   datatype kind = Itemize | Enumerate | Description
   type line
   val line_content: line -> Antiquote.text_antiquote list
-  datatype block = Paragraph of line list | List of kind * block list list
+  datatype block = Paragraph of line list | List of kind * block list
   val read_document: Input.source -> block list
 end;
 
@@ -19,20 +19,19 @@
 (* document structure *)
 
 datatype kind = Itemize | Enumerate | Description;
+type marker = {indent: int, kind: kind, pos: Position.T};
 
 datatype line =
   Line of
    {content: Antiquote.text_antiquote list,
     is_empty: bool,
-    indent: int,
-    marker: (kind * Position.T) option};
+    marker: marker option};
 
 fun line_content (Line {content, ...}) = content;
 fun line_is_empty (Line {is_empty, ...}) = is_empty;
-fun line_indent (Line {indent, ...}) = indent;
 fun line_marker (Line {marker, ...}) = marker;
 
-datatype block = Paragraph of line list | List of kind * block list list;
+datatype block = Paragraph of line list | List of kind * block list;
 
 
 (* make line *)
@@ -51,55 +50,55 @@
 fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space;
 val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
 
-val scan_prefix =
-  (Scan.many is_space >> length) --
-  Scan.option
-    ((Symbol_Pos.$$ "\<^item>" >> K Itemize ||
-      Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
-      Symbol_Pos.$$ "\<^descr>" >> K Description) -- Symbol_Pos.scan_pos);
+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));
 
-fun scan_line (Antiquote.Text ss :: _) =
-      the_default (0, NONE) (Scan.read Symbol_Pos.stopper scan_prefix ss)
-  | scan_line _ = (0, NONE);
+fun read_marker (Antiquote.Text ss :: _) =
+      #1 (Scan.finite Symbol_Pos.stopper (Scan.option scan_marker) ss)
+  | read_marker _ = NONE;
 
 in
 
 fun make_line content =
   let
     val _ = check_blanks content;
-    val (indent, marker) = scan_line content;
-  in Line {content = content, is_empty = is_empty content, indent = indent, marker = marker} end;
+    val marker = read_marker content;
+  in Line {content = content, is_empty = is_empty content, marker = marker} end;
 
 end;
 
 
-(* make blocks *)
-
-fun make_blocks spans = map Paragraph spans;
-
-
 (* read document *)
 
 local
 
 val eof =
   Line {content = [Antiquote.Text [(Symbol.eof, Position.none)]],
-    is_empty = false, indent = 0, marker = 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;
 
+val parse_paragraph = Scan.many1 plain_line >> Paragraph;
+
 val parse_span =
-  Scan.many1 plain_line || Scan.one (is_some o line_marker) -- Scan.many plain_line >> op ::;
+  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));
 
 val parse_document =
-  parse_span ::: Scan.repeat (Scan.one line_is_empty |-- parse_span) >> make_blocks;
+  parse_span ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_span) >> maps snd;
 
 val parse_documents =
-  (Scan.many line_is_empty |-- parse_document) :::
-    (Scan.repeat (Scan.many1 line_is_empty |-- parse_document) --| Scan.many line_is_empty)
-  >> flat;
+  Scan.repeat (Scan.many line_is_empty |-- parse_document) --| Scan.many line_is_empty >> flat;
 
 in