more document structure;
authorwenzelm
Thu Oct 15 12:43:02 2015 +0200 (2015-10-15)
changeset 6144531aadb15eda5
parent 61444 1fcdfc1a7e50
child 61446 9b09acfb7e06
more document structure;
tuned signature;
src/Pure/Thy/markdown.ML
     1.1 --- a/src/Pure/Thy/markdown.ML	Wed Oct 14 21:18:37 2015 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 12:43:02 2015 +0200
     1.3 @@ -7,32 +7,38 @@
     1.4  signature MARKDOWN =
     1.5  sig
     1.6    datatype kind = Itemize | Enumerate | Description
     1.7 +  type marker = {indent: int, kind: kind}
     1.8    type line
     1.9    val line_content: line -> Antiquote.text_antiquote list
    1.10 -  datatype block = Paragraph of line list | List of kind * block list
    1.11 -  val read_document: Input.source -> block list
    1.12 +  val make_line: Antiquote.text_antiquote list -> line
    1.13 +  val empty_line: line
    1.14 +  datatype block = Paragraph of line list | List of marker * block list
    1.15 +  val read_lines: line list -> block list
    1.16 +  val read: Input.source -> block list
    1.17  end;
    1.18  
    1.19  structure Markdown: MARKDOWN =
    1.20  struct
    1.21  
    1.22 -(* document structure *)
    1.23 +(* document lines *)
    1.24  
    1.25  datatype kind = Itemize | Enumerate | Description;
    1.26 -type marker = {indent: int, kind: kind, pos: Position.T};
    1.27 +type marker = {indent: int, kind: kind};
    1.28  
    1.29  datatype line =
    1.30    Line of
    1.31     {content: Antiquote.text_antiquote list,
    1.32      is_empty: bool,
    1.33 -    marker: marker option};
    1.34 +    marker: (marker * Position.T) option};
    1.35 +
    1.36 +val eof_line =
    1.37 +  Line {content = [Antiquote.Text [(Symbol.eof, Position.none)]],
    1.38 +    is_empty = false, marker = NONE};
    1.39  
    1.40  fun line_content (Line {content, ...}) = content;
    1.41  fun line_is_empty (Line {is_empty, ...}) = is_empty;
    1.42  fun line_marker (Line {marker, ...}) = marker;
    1.43  
    1.44 -datatype block = Paragraph of line list | List of kind * block list;
    1.45 -
    1.46  
    1.47  (* make line *)
    1.48  
    1.49 @@ -52,14 +58,12 @@
    1.50  
    1.51  val scan_marker =
    1.52    Scan.many is_space --
    1.53 -    (Symbol_Pos.$$ "\<^item>" >> K Itemize ||
    1.54 -     Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
    1.55 -     Symbol_Pos.$$ "\<^descr>" >> K Description)
    1.56 -    -- Symbol_Pos.scan_pos
    1.57 -    >> (fn ((a, b), c) => ({indent = length a, kind = b, pos = c}: marker));
    1.58 +  (Symbol_Pos.$$ "\<^item>" >> K Itemize ||
    1.59 +   Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
    1.60 +   Symbol_Pos.$$ "\<^descr>" >> K Description) >> (fn (a, b) => {indent = length a, kind = b});
    1.61  
    1.62  fun read_marker (Antiquote.Text ss :: _) =
    1.63 -      #1 (Scan.finite Symbol_Pos.stopper (Scan.option scan_marker) ss)
    1.64 +      #1 (Scan.finite Symbol_Pos.stopper (Scan.option (scan_marker -- Symbol_Pos.scan_pos)) ss)
    1.65    | read_marker _ = NONE;
    1.66  
    1.67  in
    1.68 @@ -70,21 +74,30 @@
    1.69      val marker = read_marker content;
    1.70    in Line {content = content, is_empty = is_empty content, marker = marker} end;
    1.71  
    1.72 +val empty_line = make_line [];
    1.73 +
    1.74  end;
    1.75  
    1.76  
    1.77 +(* document blocks *)
    1.78 +
    1.79 +datatype block = Paragraph of line list | List of marker * block list;
    1.80 +
    1.81 +fun add_span (opt_marker, body) document =
    1.82 +  (case (opt_marker, document) of
    1.83 +    (SOME marker, List (list_marker, list_body) :: rest) =>
    1.84 +      if marker = list_marker then List (list_marker, body @ list_body) :: rest
    1.85 +      else List (marker, body) :: document
    1.86 +  | (SOME marker, _) => List (marker, body) :: document
    1.87 +  | (NONE, _) => body @ document);
    1.88 +
    1.89 +
    1.90  (* read document *)
    1.91  
    1.92  local
    1.93  
    1.94 -val eof =
    1.95 -  Line {content = [Antiquote.Text [(Symbol.eof, Position.none)]],
    1.96 -    is_empty = false, marker = NONE};
    1.97 -
    1.98 -val stopper = Scan.stopper (K eof) (fn line => line = eof);
    1.99 -
   1.100  fun plain_line line =
   1.101 -  not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof;
   1.102 +  not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof_line;
   1.103  
   1.104  val parse_paragraph = Scan.many1 plain_line >> Paragraph;
   1.105  
   1.106 @@ -92,20 +105,22 @@
   1.107    parse_paragraph >> (fn par => (NONE, [par])) ||
   1.108    Scan.one (is_some o line_marker) -- Scan.many plain_line --
   1.109      Scan.repeat (Scan.one line_is_empty |-- parse_paragraph) >>
   1.110 -      (fn ((line, lines), pars) => ((line_marker line), Paragraph (line :: lines) :: pars));
   1.111 +      (fn ((line, lines), pars) =>
   1.112 +        (Option.map #1 (line_marker line), Paragraph (line :: lines) :: pars));
   1.113  
   1.114  val parse_document =
   1.115 -  parse_span ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_span) >> maps snd;
   1.116 -
   1.117 -val parse_documents =
   1.118 -  Scan.repeat (Scan.many line_is_empty |-- parse_document) --| Scan.many line_is_empty >> flat;
   1.119 +  parse_span ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_span)
   1.120 +    >> (fn spans => fold_rev add_span spans []);
   1.121  
   1.122  in
   1.123  
   1.124 -val read_document =
   1.125 -  Antiquote.read #> Antiquote.split_lines #> map make_line #>
   1.126 -  Scan.read stopper parse_documents #> the_default [];
   1.127 +val read_lines =
   1.128 +  Scan.read (Scan.stopper (K eof_line) (fn line => line = eof_line))
   1.129 +    (Scan.repeat (Scan.many line_is_empty |-- parse_document) --| Scan.many line_is_empty) #>
   1.130 +  the_default [] #> flat;
   1.131  
   1.132  end;
   1.133  
   1.134 +val read = Antiquote.read #> Antiquote.split_lines #> map make_line #> read_lines;
   1.135 +
   1.136  end;