61441
|
1 |
(* Title: Pure/Thy/markdown.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
61448
|
4 |
Minimal support for Markdown documents (see also http://commonmark.org)
|
|
5 |
that consist only of paragraphs and (nested) lists:
|
|
6 |
|
|
7 |
* list items start with marker \<^item> (itemize), \<^enum> (enumerate), \<^descr> (description)
|
|
8 |
* adjacent list items with same indentation and same marker are grouped
|
|
9 |
into a single list
|
|
10 |
* singleton blank lines separate paragraphs
|
|
11 |
* multiple blank lines escape from the current list hierarchy
|
|
12 |
|
|
13 |
Notable differences to official Markdown:
|
|
14 |
|
|
15 |
* indentation of list items needs to match exactly
|
|
16 |
* indentation is unlimited (Markdown interprets 4 spaces as block quote)
|
|
17 |
* list items always consist of paragraphs -- no notion of "tight" list
|
61441
|
18 |
*)
|
|
19 |
|
|
20 |
signature MARKDOWN =
|
|
21 |
sig
|
61443
|
22 |
datatype kind = Itemize | Enumerate | Description
|
61449
|
23 |
val print_kind: kind -> string
|
61445
|
24 |
type marker = {indent: int, kind: kind}
|
61441
|
25 |
type line
|
61443
|
26 |
val line_content: line -> Antiquote.text_antiquote list
|
61445
|
27 |
val make_line: Antiquote.text_antiquote list -> line
|
|
28 |
val empty_line: line
|
|
29 |
datatype block = Paragraph of line list | List of marker * block list
|
|
30 |
val read_lines: line list -> block list
|
|
31 |
val read: Input.source -> block list
|
61449
|
32 |
val reports: block list -> Position.report list
|
61441
|
33 |
end;
|
|
34 |
|
|
35 |
structure Markdown: MARKDOWN =
|
|
36 |
struct
|
|
37 |
|
61445
|
38 |
(* document lines *)
|
61441
|
39 |
|
|
40 |
datatype kind = Itemize | Enumerate | Description;
|
61449
|
41 |
|
|
42 |
fun print_kind Itemize = "itemize"
|
|
43 |
| print_kind Enumerate = "enumerate"
|
|
44 |
| print_kind Description = "description";
|
|
45 |
|
61445
|
46 |
type marker = {indent: int, kind: kind};
|
61441
|
47 |
|
|
48 |
datatype line =
|
|
49 |
Line of
|
|
50 |
{content: Antiquote.text_antiquote list,
|
|
51 |
is_empty: bool,
|
61445
|
52 |
marker: (marker * Position.T) option};
|
|
53 |
|
|
54 |
val eof_line =
|
|
55 |
Line {content = [Antiquote.Text [(Symbol.eof, Position.none)]],
|
|
56 |
is_empty = false, marker = NONE};
|
61441
|
57 |
|
|
58 |
fun line_content (Line {content, ...}) = content;
|
|
59 |
fun line_is_empty (Line {is_empty, ...}) = is_empty;
|
|
60 |
fun line_marker (Line {marker, ...}) = marker;
|
|
61 |
|
61443
|
62 |
|
|
63 |
(* make line *)
|
|
64 |
|
61441
|
65 |
local
|
|
66 |
|
|
67 |
fun bad_blank ((s, _): Symbol_Pos.T) = Symbol.is_ascii_blank s andalso s <> Symbol.space;
|
|
68 |
val bad_blanks = maps (fn Antiquote.Text ss => filter bad_blank ss | _ => []);
|
|
69 |
|
|
70 |
fun check_blanks content =
|
|
71 |
(case bad_blanks content of
|
|
72 |
[] => ()
|
|
73 |
| (c, pos) :: _ =>
|
|
74 |
error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos));
|
|
75 |
|
|
76 |
fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space;
|
|
77 |
val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
|
|
78 |
|
61444
|
79 |
val scan_marker =
|
61449
|
80 |
Scan.many is_space -- Symbol_Pos.scan_pos --
|
61445
|
81 |
(Symbol_Pos.$$ "\<^item>" >> K Itemize ||
|
|
82 |
Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
|
61449
|
83 |
Symbol_Pos.$$ "\<^descr>" >> K Description)
|
|
84 |
>> (fn ((spaces, pos), kind) => ({indent = length spaces, kind = kind}, pos));
|
61442
|
85 |
|
61444
|
86 |
fun read_marker (Antiquote.Text ss :: _) =
|
61449
|
87 |
#1 (Scan.finite Symbol_Pos.stopper (Scan.option scan_marker) ss)
|
61444
|
88 |
| read_marker _ = NONE;
|
61441
|
89 |
|
|
90 |
in
|
|
91 |
|
|
92 |
fun make_line content =
|
|
93 |
let
|
|
94 |
val _ = check_blanks content;
|
61444
|
95 |
val marker = read_marker content;
|
|
96 |
in Line {content = content, is_empty = is_empty content, marker = marker} end;
|
61441
|
97 |
|
61445
|
98 |
val empty_line = make_line [];
|
|
99 |
|
61441
|
100 |
end;
|
|
101 |
|
|
102 |
|
61445
|
103 |
(* document blocks *)
|
|
104 |
|
|
105 |
datatype block = Paragraph of line list | List of marker * block list;
|
|
106 |
|
61450
|
107 |
fun block_lines (Paragraph lines) = lines
|
|
108 |
| block_lines (List (_, blocks)) = maps block_lines blocks;
|
|
109 |
|
|
110 |
|
61445
|
111 |
fun add_span (opt_marker, body) document =
|
|
112 |
(case (opt_marker, document) of
|
61446
|
113 |
(SOME marker, (list as List (list_marker, list_body)) :: rest) =>
|
|
114 |
if marker = list_marker then
|
|
115 |
List (list_marker, body @ list_body) :: rest
|
|
116 |
else if #indent marker < #indent list_marker then
|
|
117 |
List (marker, body @ [list]) :: rest
|
|
118 |
else
|
|
119 |
List (marker, body) :: document
|
61445
|
120 |
| (SOME marker, _) => List (marker, body) :: document
|
|
121 |
| (NONE, _) => body @ document);
|
|
122 |
|
|
123 |
|
61443
|
124 |
(* read document *)
|
61441
|
125 |
|
|
126 |
local
|
|
127 |
|
61442
|
128 |
fun plain_line line =
|
61445
|
129 |
not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof_line;
|
61441
|
130 |
|
61444
|
131 |
val parse_paragraph = Scan.many1 plain_line >> Paragraph;
|
|
132 |
|
61441
|
133 |
val parse_span =
|
61444
|
134 |
parse_paragraph >> (fn par => (NONE, [par])) ||
|
|
135 |
Scan.one (is_some o line_marker) -- Scan.many plain_line --
|
|
136 |
Scan.repeat (Scan.one line_is_empty |-- parse_paragraph) >>
|
61445
|
137 |
(fn ((line, lines), pars) =>
|
|
138 |
(Option.map #1 (line_marker line), Paragraph (line :: lines) :: pars));
|
61443
|
139 |
|
|
140 |
val parse_document =
|
61445
|
141 |
parse_span ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_span)
|
|
142 |
>> (fn spans => fold_rev add_span spans []);
|
61441
|
143 |
|
|
144 |
in
|
|
145 |
|
61445
|
146 |
val read_lines =
|
|
147 |
Scan.read (Scan.stopper (K eof_line) (fn line => line = eof_line))
|
|
148 |
(Scan.repeat (Scan.many line_is_empty |-- parse_document) --| Scan.many line_is_empty) #>
|
|
149 |
the_default [] #> flat;
|
61441
|
150 |
|
|
151 |
end;
|
|
152 |
|
61445
|
153 |
val read = Antiquote.read #> Antiquote.split_lines #> map make_line #> read_lines;
|
|
154 |
|
61449
|
155 |
|
|
156 |
(* PIDE reports *)
|
|
157 |
|
|
158 |
local
|
|
159 |
|
|
160 |
fun line_reports depth (Line {marker = SOME (_, pos), ...}) =
|
61450
|
161 |
cons (pos, Markup.markdown_item depth)
|
61449
|
162 |
| line_reports _ _ = I;
|
|
163 |
|
61450
|
164 |
val lines_pos = #1 o Antiquote.range o maps line_content;
|
|
165 |
|
|
166 |
fun block_reports depth (Paragraph lines) =
|
|
167 |
cons (lines_pos lines, Markup.markdown_paragraph) #>
|
|
168 |
fold (line_reports depth) lines
|
|
169 |
| block_reports depth (List ({kind, ...}, body)) =
|
|
170 |
cons (lines_pos (maps block_lines body), Markup.markdown_list (print_kind kind)) #>
|
|
171 |
fold (block_reports (depth + 1)) body;
|
61449
|
172 |
|
|
173 |
in
|
|
174 |
|
61450
|
175 |
fun reports blocks =
|
|
176 |
filter (Position.is_reported o #1) (fold (block_reports 0) blocks []);
|
61449
|
177 |
|
61441
|
178 |
end;
|
61449
|
179 |
|
|
180 |
end;
|