more document structure;
authorwenzelm
Wed Oct 14 21:18:37 2015 +0200 (2015-10-14)
changeset 614441fcdfc1a7e50
parent 61443 78bbfadd1034
child 61445 31aadb15eda5
more document structure;
src/Pure/Thy/markdown.ML
     1.1 --- a/src/Pure/Thy/markdown.ML	Wed Oct 14 19:44:43 2015 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Wed Oct 14 21:18:37 2015 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4    datatype kind = Itemize | Enumerate | Description
     1.5    type line
     1.6    val line_content: line -> Antiquote.text_antiquote list
     1.7 -  datatype block = Paragraph of line list | List of kind * block list list
     1.8 +  datatype block = Paragraph of line list | List of kind * block list
     1.9    val read_document: Input.source -> block list
    1.10  end;
    1.11  
    1.12 @@ -19,20 +19,19 @@
    1.13  (* document structure *)
    1.14  
    1.15  datatype kind = Itemize | Enumerate | Description;
    1.16 +type marker = {indent: int, kind: kind, pos: Position.T};
    1.17  
    1.18  datatype line =
    1.19    Line of
    1.20     {content: Antiquote.text_antiquote list,
    1.21      is_empty: bool,
    1.22 -    indent: int,
    1.23 -    marker: (kind * Position.T) option};
    1.24 +    marker: marker option};
    1.25  
    1.26  fun line_content (Line {content, ...}) = content;
    1.27  fun line_is_empty (Line {is_empty, ...}) = is_empty;
    1.28 -fun line_indent (Line {indent, ...}) = indent;
    1.29  fun line_marker (Line {marker, ...}) = marker;
    1.30  
    1.31 -datatype block = Paragraph of line list | List of kind * block list list;
    1.32 +datatype block = Paragraph of line list | List of kind * block list;
    1.33  
    1.34  
    1.35  (* make line *)
    1.36 @@ -51,55 +50,55 @@
    1.37  fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space;
    1.38  val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
    1.39  
    1.40 -val scan_prefix =
    1.41 -  (Scan.many is_space >> length) --
    1.42 -  Scan.option
    1.43 -    ((Symbol_Pos.$$ "\<^item>" >> K Itemize ||
    1.44 -      Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
    1.45 -      Symbol_Pos.$$ "\<^descr>" >> K Description) -- Symbol_Pos.scan_pos);
    1.46 +val scan_marker =
    1.47 +  Scan.many is_space --
    1.48 +    (Symbol_Pos.$$ "\<^item>" >> K Itemize ||
    1.49 +     Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
    1.50 +     Symbol_Pos.$$ "\<^descr>" >> K Description)
    1.51 +    -- Symbol_Pos.scan_pos
    1.52 +    >> (fn ((a, b), c) => ({indent = length a, kind = b, pos = c}: marker));
    1.53  
    1.54 -fun scan_line (Antiquote.Text ss :: _) =
    1.55 -      the_default (0, NONE) (Scan.read Symbol_Pos.stopper scan_prefix ss)
    1.56 -  | scan_line _ = (0, NONE);
    1.57 +fun read_marker (Antiquote.Text ss :: _) =
    1.58 +      #1 (Scan.finite Symbol_Pos.stopper (Scan.option scan_marker) ss)
    1.59 +  | read_marker _ = NONE;
    1.60  
    1.61  in
    1.62  
    1.63  fun make_line content =
    1.64    let
    1.65      val _ = check_blanks content;
    1.66 -    val (indent, marker) = scan_line content;
    1.67 -  in Line {content = content, is_empty = is_empty content, indent = indent, marker = marker} end;
    1.68 +    val marker = read_marker content;
    1.69 +  in Line {content = content, is_empty = is_empty content, marker = marker} end;
    1.70  
    1.71  end;
    1.72  
    1.73  
    1.74 -(* make blocks *)
    1.75 -
    1.76 -fun make_blocks spans = map Paragraph spans;
    1.77 -
    1.78 -
    1.79  (* read document *)
    1.80  
    1.81  local
    1.82  
    1.83  val eof =
    1.84    Line {content = [Antiquote.Text [(Symbol.eof, Position.none)]],
    1.85 -    is_empty = false, indent = 0, marker = NONE};
    1.86 +    is_empty = false, marker = NONE};
    1.87 +
    1.88  val stopper = Scan.stopper (K eof) (fn line => line = eof);
    1.89  
    1.90  fun plain_line line =
    1.91    not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof;
    1.92  
    1.93 +val parse_paragraph = Scan.many1 plain_line >> Paragraph;
    1.94 +
    1.95  val parse_span =
    1.96 -  Scan.many1 plain_line || Scan.one (is_some o line_marker) -- Scan.many plain_line >> op ::;
    1.97 +  parse_paragraph >> (fn par => (NONE, [par])) ||
    1.98 +  Scan.one (is_some o line_marker) -- Scan.many plain_line --
    1.99 +    Scan.repeat (Scan.one line_is_empty |-- parse_paragraph) >>
   1.100 +      (fn ((line, lines), pars) => ((line_marker line), Paragraph (line :: lines) :: pars));
   1.101  
   1.102  val parse_document =
   1.103 -  parse_span ::: Scan.repeat (Scan.one line_is_empty |-- parse_span) >> make_blocks;
   1.104 +  parse_span ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_span) >> maps snd;
   1.105  
   1.106  val parse_documents =
   1.107 -  (Scan.many line_is_empty |-- parse_document) :::
   1.108 -    (Scan.repeat (Scan.many1 line_is_empty |-- parse_document) --| Scan.many line_is_empty)
   1.109 -  >> flat;
   1.110 +  Scan.repeat (Scan.many line_is_empty |-- parse_document) --| Scan.many line_is_empty >> flat;
   1.111  
   1.112  in
   1.113