more document structure;
authorwenzelm
Wed Oct 14 19:44:43 2015 +0200 (2015-10-14)
changeset 6144378bbfadd1034
parent 61442 467ebb937294
child 61444 1fcdfc1a7e50
more document structure;
src/Pure/Thy/markdown.ML
     1.1 --- a/src/Pure/Thy/markdown.ML	Wed Oct 14 18:29:41 2015 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Wed Oct 14 19:44:43 2015 +0200
     1.3 @@ -6,14 +6,17 @@
     1.4  
     1.5  signature MARKDOWN =
     1.6  sig
     1.7 +  datatype kind = Itemize | Enumerate | Description
     1.8    type line
     1.9 -  val read: Input.source -> line list list
    1.10 +  val line_content: line -> Antiquote.text_antiquote list
    1.11 +  datatype block = Paragraph of line list | List of kind * block list list
    1.12 +  val read_document: Input.source -> block list
    1.13  end;
    1.14  
    1.15  structure Markdown: MARKDOWN =
    1.16  struct
    1.17  
    1.18 -(* line with optional item marker *)
    1.19 +(* document structure *)
    1.20  
    1.21  datatype kind = Itemize | Enumerate | Description;
    1.22  
    1.23 @@ -29,6 +32,11 @@
    1.24  fun line_indent (Line {indent, ...}) = indent;
    1.25  fun line_marker (Line {marker, ...}) = marker;
    1.26  
    1.27 +datatype block = Paragraph of line list | List of kind * block list list;
    1.28 +
    1.29 +
    1.30 +(* make line *)
    1.31 +
    1.32  local
    1.33  
    1.34  fun bad_blank ((s, _): Symbol_Pos.T) = Symbol.is_ascii_blank s andalso s <> Symbol.space;
    1.35 @@ -65,7 +73,12 @@
    1.36  end;
    1.37  
    1.38  
    1.39 -(* spans of related lines *)
    1.40 +(* make blocks *)
    1.41 +
    1.42 +fun make_blocks spans = map Paragraph spans;
    1.43 +
    1.44 +
    1.45 +(* read document *)
    1.46  
    1.47  local
    1.48  
    1.49 @@ -78,24 +91,22 @@
    1.50    not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof;
    1.51  
    1.52  val parse_span =
    1.53 -  Scan.many1 plain_line ||
    1.54 -  Scan.one (is_some o line_marker) -- Scan.many plain_line >> op :: ||
    1.55 -  Scan.many1 line_is_empty;
    1.56 +  Scan.many1 plain_line || Scan.one (is_some o line_marker) -- Scan.many plain_line >> op ::;
    1.57 +
    1.58 +val parse_document =
    1.59 +  parse_span ::: Scan.repeat (Scan.one line_is_empty |-- parse_span) >> make_blocks;
    1.60 +
    1.61 +val parse_documents =
    1.62 +  (Scan.many line_is_empty |-- parse_document) :::
    1.63 +    (Scan.repeat (Scan.many1 line_is_empty |-- parse_document) --| Scan.many line_is_empty)
    1.64 +  >> flat;
    1.65  
    1.66  in
    1.67  
    1.68 -fun read_spans lines =
    1.69 -  the_default [] (Scan.read stopper (Scan.repeat parse_span) lines);
    1.70 +val read_document =
    1.71 +  Antiquote.read #> Antiquote.split_lines #> map make_line #>
    1.72 +  Scan.read stopper parse_documents #> the_default [];
    1.73  
    1.74  end;
    1.75  
    1.76 -
    1.77 -(* document structure *)
    1.78 -
    1.79 -fun read input =
    1.80 -  Antiquote.read input
    1.81 -  |> Antiquote.split_lines
    1.82 -  |> map make_line
    1.83 -  |> read_spans;
    1.84 -
    1.85  end;