src/Pure/Thy/markdown.ML
changeset 61459 5f2ddeb15c06
parent 61457 3e21699bb83b
child 61460 732028edfbc7
     1.1 --- a/src/Pure/Thy/markdown.ML	Fri Oct 16 14:53:26 2015 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Sat Oct 17 19:26:34 2015 +0200
     1.3 @@ -22,13 +22,12 @@
     1.4    val is_control: Symbol.symbol -> bool
     1.5    datatype kind = Itemize | Enumerate | Description
     1.6    val print_kind: kind -> string
     1.7 -  type marker = {indent: int, kind: kind}
     1.8    type line
     1.9    val line_source: line -> Antiquote.text_antiquote list
    1.10    val line_content: line -> Antiquote.text_antiquote list
    1.11    val make_line: Antiquote.text_antiquote list -> line
    1.12    val empty_line: line
    1.13 -  datatype block = Paragraph of line list | List of marker * block list
    1.14 +  datatype block = Paragraph of line list | List of {indent: int, kind: kind, body: block list}
    1.15    val read_lines: line list -> block list
    1.16    val read_antiquotes: Antiquote.text_antiquote list -> block list
    1.17    val read_source: Input.source -> block list
    1.18 @@ -49,23 +48,25 @@
    1.19    | print_kind Enumerate = "enumerate"
    1.20    | print_kind Description = "description";
    1.21  
    1.22 -type marker = {indent: int, kind: kind};
    1.23 -
    1.24  datatype line =
    1.25    Line of
    1.26     {source: Antiquote.text_antiquote list,
    1.27 -    content: Antiquote.text_antiquote list,
    1.28      is_empty: bool,
    1.29 -    marker: (marker * Position.T) option};
    1.30 +    indent: int,
    1.31 +    item: kind option,
    1.32 +    item_pos: Position.T,
    1.33 +    content: Antiquote.text_antiquote list};
    1.34  
    1.35  val eof_line =
    1.36    Line {source = [Antiquote.Text [(Symbol.eof, Position.none)]],
    1.37 -    content = [], is_empty = false, marker = NONE};
    1.38 +    is_empty = false, indent = 0, item = NONE, item_pos = Position.none, content = []};
    1.39  
    1.40  fun line_source (Line {source, ...}) = source;
    1.41 +fun line_is_empty (Line {is_empty, ...}) = is_empty;
    1.42 +fun line_indent (Line {indent, ...}) = indent;
    1.43 +fun line_item (Line {item, ...}) = item;
    1.44 +fun line_item_pos (Line {item_pos, ...}) = item_pos;
    1.45  fun line_content (Line {content, ...}) = content;
    1.46 -fun line_is_empty (Line {is_empty, ...}) = is_empty;
    1.47 -fun line_marker (Line {marker, ...}) = marker;
    1.48  
    1.49  
    1.50  (* make line *)
    1.51 @@ -86,24 +87,28 @@
    1.52  
    1.53  val scan_marker =
    1.54    Scan.many is_space -- Symbol_Pos.scan_pos --
    1.55 -  (Symbol_Pos.$$ "\\<^item>" >> K Itemize ||
    1.56 -   Symbol_Pos.$$ "\\<^enum>" >> K Enumerate ||
    1.57 -   Symbol_Pos.$$ "\\<^descr>" >> K Description)
    1.58 -  >> (fn ((spaces, pos), kind) => ({indent = length spaces, kind = kind}, pos));
    1.59 +  Scan.option
    1.60 +   (Symbol_Pos.$$ "\\<^item>" >> K Itemize ||
    1.61 +    Symbol_Pos.$$ "\\<^enum>" >> K Enumerate ||
    1.62 +    Symbol_Pos.$$ "\\<^descr>" >> K Description) --| Scan.many is_space
    1.63 +  >> (fn ((sp, pos), item) => (length sp, item, if is_some item then pos else Position.none));
    1.64  
    1.65  fun read_marker (Antiquote.Text ss :: rest) =
    1.66 -      (case Scan.finite Symbol_Pos.stopper (Scan.option scan_marker --| Scan.many is_space) ss of
    1.67 +      (case Scan.finite Symbol_Pos.stopper scan_marker ss of
    1.68          (marker, []) => (marker, rest)
    1.69        | (marker, ss') => (marker, Antiquote.Text ss' :: rest))
    1.70 -  | read_marker source = (NONE, source);
    1.71 +  | read_marker source = ((0, NONE, Position.none), source);
    1.72  
    1.73  in
    1.74  
    1.75  fun make_line source =
    1.76    let
    1.77      val _ = check_blanks source;
    1.78 -    val (marker, content) = read_marker source;
    1.79 -  in Line {source = source, content = content, is_empty = is_empty source, marker = marker} end;
    1.80 +    val ((indent, item, item_pos), content) = read_marker source;
    1.81 +  in
    1.82 +    Line {source = source, is_empty = is_empty source, indent = indent,
    1.83 +      item = item, item_pos = item_pos, content = content}
    1.84 +  end;
    1.85  
    1.86  val empty_line = make_line [];
    1.87  
    1.88 @@ -112,46 +117,53 @@
    1.89  
    1.90  (* document blocks *)
    1.91  
    1.92 -datatype block = Paragraph of line list | List of marker * block list;
    1.93 +datatype block =
    1.94 +  Paragraph of line list | List of {indent: int, kind: kind, body: block list};
    1.95  
    1.96  fun block_lines (Paragraph lines) = lines
    1.97 -  | block_lines (List (_, blocks)) = maps block_lines blocks;
    1.98 +  | block_lines (List {body, ...}) = maps block_lines body;
    1.99  
   1.100  fun block_range (Paragraph lines) = Antiquote.range (maps line_content lines)
   1.101 -  | block_range (List (_, blocks)) = Antiquote.range (maps line_source (maps block_lines blocks));
   1.102 +  | block_range (List {body, ...}) = Antiquote.range (maps line_source (maps block_lines body));
   1.103 +
   1.104 +fun block_indent (List {indent, ...}) = indent
   1.105 +  | block_indent (Paragraph (line :: _)) = line_indent line
   1.106 +  | block_indent _ = 0;
   1.107 +
   1.108 +fun block_list indent0 kind0 (List {indent, kind, body}) =
   1.109 +      if indent0 = indent andalso kind0 = kind then SOME body else NONE
   1.110 +  | block_list _ _ _ = NONE;
   1.111 +
   1.112 +val is_list = fn List _ => true | _ => false;
   1.113  
   1.114  
   1.115  (* read document *)
   1.116  
   1.117  local
   1.118  
   1.119 -fun add_span (opt_marker, body) document =
   1.120 -  (case (opt_marker, document) of
   1.121 -    (SOME marker, (list as List (list_marker, list_body)) :: rest) =>
   1.122 -      if marker = list_marker then
   1.123 -        List (list_marker, body @ list_body) :: rest
   1.124 -      else if #indent marker < #indent list_marker then
   1.125 -        add_span (opt_marker, body @ [list]) rest
   1.126 -      else
   1.127 -        List (marker, body) :: document
   1.128 -  | (SOME marker, _) => List (marker, body) :: document
   1.129 -  | (NONE, _) => body @ document);
   1.130 +fun build (indent, item, rev_body) document =
   1.131 +  (case (item, document) of
   1.132 +    (SOME kind, block :: blocks) =>
   1.133 +      (case block_list indent kind block of
   1.134 +        SOME list => List {indent = indent, kind = kind, body = fold cons rev_body list} :: blocks
   1.135 +      | NONE =>
   1.136 +          if (if is_list block then indent < block_indent block else indent <= block_indent block)
   1.137 +          then build (indent, item, block :: rev_body) blocks
   1.138 +          else List {indent = indent, kind = kind, body = rev rev_body} :: document)
   1.139 +  | (SOME kind, []) => [List {indent = indent, kind = kind, body = rev rev_body}]
   1.140 +  | (NONE, _) => fold cons rev_body document);
   1.141  
   1.142  fun plain_line line =
   1.143 -  not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof_line;
   1.144 -
   1.145 -val parse_paragraph = Scan.many1 plain_line >> Paragraph;
   1.146 +  not (line_is_empty line) andalso is_none (line_item line) andalso line <> eof_line;
   1.147  
   1.148 -val parse_span =
   1.149 -  parse_paragraph >> (fn par => (NONE, [par])) ||
   1.150 -  Scan.one (is_some o line_marker) -- Scan.many plain_line --
   1.151 -    Scan.repeat (Scan.one line_is_empty |-- parse_paragraph) >>
   1.152 -      (fn ((line, lines), pars) =>
   1.153 -        (Option.map #1 (line_marker line), Paragraph (line :: lines) :: pars));
   1.154 +val parse_paragraph =
   1.155 +  Scan.one (fn line => line <> eof_line) -- Scan.many plain_line >> (fn (line, lines) =>
   1.156 +    let val block = Paragraph (line :: lines)
   1.157 +    in (line_indent line, line_item line, [block]) end);
   1.158  
   1.159  val parse_document =
   1.160 -  parse_span ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_span)
   1.161 -    >> (fn spans => fold_rev add_span spans []);
   1.162 +  parse_paragraph ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_paragraph)
   1.163 +    >> (fn pars => fold_rev build pars []);
   1.164  
   1.165  in
   1.166  
   1.167 @@ -173,17 +185,16 @@
   1.168  
   1.169  local
   1.170  
   1.171 -fun line_reports depth (Line {marker = SOME (_, pos), content, ...}) =
   1.172 -      cons (pos, Markup.markdown_item depth) #>
   1.173 -      append (text_reports content)
   1.174 -  | line_reports _ _ = I;
   1.175 +fun line_reports depth line =
   1.176 +  cons (line_item_pos line, Markup.markdown_item depth) #>
   1.177 +  append (text_reports (line_content line));
   1.178  
   1.179  fun block_reports depth block =
   1.180    (case block of
   1.181      Paragraph lines =>
   1.182        cons (#1 (block_range block), Markup.markdown_paragraph) #>
   1.183        fold (line_reports depth) lines
   1.184 -  | List ({kind, ...}, body) =>
   1.185 +  | List {kind, body, ...} =>
   1.186        cons (#1 (block_range block), Markup.markdown_list (print_kind kind)) #>
   1.187        fold (block_reports (depth + 1)) body);
   1.188