author | wenzelm |
Sat, 17 Oct 2015 19:47:34 +0200 | |
changeset 61461 | 77c9643a6353 |
parent 61460 | 732028edfbc7 |
child 61595 | 3591274c607e |
permissions | -rw-r--r-- |
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 |
|
61457 | 22 |
val is_control: Symbol.symbol -> bool |
61443 | 23 |
datatype kind = Itemize | Enumerate | Description |
61449 | 24 |
val print_kind: kind -> string |
61441 | 25 |
type line |
61451
7f530057bc3c
clarified line content: source without marker prefix;
wenzelm
parents:
61450
diff
changeset
|
26 |
val line_source: line -> Antiquote.text_antiquote list |
61461 | 27 |
val line_is_item: line -> bool |
61443 | 28 |
val line_content: line -> Antiquote.text_antiquote list |
61445 | 29 |
val make_line: Antiquote.text_antiquote list -> line |
30 |
val empty_line: line |
|
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
31 |
datatype block = Paragraph of line list | List of {indent: int, kind: kind, body: block list} |
61445 | 32 |
val read_lines: line list -> block list |
61457 | 33 |
val read_antiquotes: Antiquote.text_antiquote list -> block list |
34 |
val read_source: Input.source -> block list |
|
35 |
val text_reports: Antiquote.text_antiquote list -> Position.report list |
|
61449 | 36 |
val reports: block list -> Position.report list |
61441 | 37 |
end; |
38 |
||
39 |
structure Markdown: MARKDOWN = |
|
40 |
struct |
|
41 |
||
61445 | 42 |
(* document lines *) |
61441 | 43 |
|
61457 | 44 |
val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"]; |
45 |
||
61441 | 46 |
datatype kind = Itemize | Enumerate | Description; |
61449 | 47 |
|
48 |
fun print_kind Itemize = "itemize" |
|
49 |
| print_kind Enumerate = "enumerate" |
|
50 |
| print_kind Description = "description"; |
|
51 |
||
61441 | 52 |
datatype line = |
53 |
Line of |
|
61451
7f530057bc3c
clarified line content: source without marker prefix;
wenzelm
parents:
61450
diff
changeset
|
54 |
{source: Antiquote.text_antiquote list, |
61441 | 55 |
is_empty: bool, |
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
56 |
indent: int, |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
57 |
item: kind option, |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
58 |
item_pos: Position.T, |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
59 |
content: Antiquote.text_antiquote list}; |
61445 | 60 |
|
61 |
val eof_line = |
|
61451
7f530057bc3c
clarified line content: source without marker prefix;
wenzelm
parents:
61450
diff
changeset
|
62 |
Line {source = [Antiquote.Text [(Symbol.eof, Position.none)]], |
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
63 |
is_empty = false, indent = 0, item = NONE, item_pos = Position.none, content = []}; |
61441 | 64 |
|
61451
7f530057bc3c
clarified line content: source without marker prefix;
wenzelm
parents:
61450
diff
changeset
|
65 |
fun line_source (Line {source, ...}) = source; |
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
66 |
fun line_is_empty (Line {is_empty, ...}) = is_empty; |
61461 | 67 |
fun line_is_item (Line {item, ...}) = is_some item; |
61441 | 68 |
fun line_content (Line {content, ...}) = content; |
69 |
||
61443 | 70 |
|
71 |
(* make line *) |
|
72 |
||
61441 | 73 |
local |
74 |
||
75 |
fun bad_blank ((s, _): Symbol_Pos.T) = Symbol.is_ascii_blank s andalso s <> Symbol.space; |
|
76 |
val bad_blanks = maps (fn Antiquote.Text ss => filter bad_blank ss | _ => []); |
|
77 |
||
61451
7f530057bc3c
clarified line content: source without marker prefix;
wenzelm
parents:
61450
diff
changeset
|
78 |
fun check_blanks source = |
7f530057bc3c
clarified line content: source without marker prefix;
wenzelm
parents:
61450
diff
changeset
|
79 |
(case bad_blanks source of |
61441 | 80 |
[] => () |
81 |
| (c, pos) :: _ => |
|
82 |
error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos)); |
|
83 |
||
84 |
fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space; |
|
85 |
val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false); |
|
86 |
||
61444 | 87 |
val scan_marker = |
61449 | 88 |
Scan.many is_space -- Symbol_Pos.scan_pos -- |
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
89 |
Scan.option |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
90 |
(Symbol_Pos.$$ "\\<^item>" >> K Itemize || |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
91 |
Symbol_Pos.$$ "\\<^enum>" >> K Enumerate || |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
92 |
Symbol_Pos.$$ "\\<^descr>" >> K Description) --| Scan.many is_space |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
93 |
>> (fn ((sp, pos), item) => (length sp, item, if is_some item then pos else Position.none)); |
61442 | 94 |
|
61451
7f530057bc3c
clarified line content: source without marker prefix;
wenzelm
parents:
61450
diff
changeset
|
95 |
fun read_marker (Antiquote.Text ss :: rest) = |
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
96 |
(case Scan.finite Symbol_Pos.stopper scan_marker ss of |
61451
7f530057bc3c
clarified line content: source without marker prefix;
wenzelm
parents:
61450
diff
changeset
|
97 |
(marker, []) => (marker, rest) |
7f530057bc3c
clarified line content: source without marker prefix;
wenzelm
parents:
61450
diff
changeset
|
98 |
| (marker, ss') => (marker, Antiquote.Text ss' :: rest)) |
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
99 |
| read_marker source = ((0, NONE, Position.none), source); |
61441 | 100 |
|
101 |
in |
|
102 |
||
61451
7f530057bc3c
clarified line content: source without marker prefix;
wenzelm
parents:
61450
diff
changeset
|
103 |
fun make_line source = |
61441 | 104 |
let |
61451
7f530057bc3c
clarified line content: source without marker prefix;
wenzelm
parents:
61450
diff
changeset
|
105 |
val _ = check_blanks source; |
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
106 |
val ((indent, item, item_pos), content) = read_marker source; |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
107 |
in |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
108 |
Line {source = source, is_empty = is_empty source, indent = indent, |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
109 |
item = item, item_pos = item_pos, content = content} |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
110 |
end; |
61441 | 111 |
|
61445 | 112 |
val empty_line = make_line []; |
113 |
||
61441 | 114 |
end; |
115 |
||
116 |
||
61445 | 117 |
(* document blocks *) |
118 |
||
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
119 |
datatype block = |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
120 |
Paragraph of line list | List of {indent: int, kind: kind, body: block list}; |
61445 | 121 |
|
61450 | 122 |
fun block_lines (Paragraph lines) = lines |
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
123 |
| block_lines (List {body, ...}) = maps block_lines body; |
61450 | 124 |
|
61452 | 125 |
fun block_range (Paragraph lines) = Antiquote.range (maps line_content lines) |
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
126 |
| block_range (List {body, ...}) = Antiquote.range (maps line_source (maps block_lines body)); |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
127 |
|
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
128 |
fun block_indent (List {indent, ...}) = indent |
61460 | 129 |
| block_indent (Paragraph (Line {indent, ...} :: _)) = indent |
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
130 |
| block_indent _ = 0; |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
131 |
|
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
132 |
fun block_list indent0 kind0 (List {indent, kind, body}) = |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
133 |
if indent0 = indent andalso kind0 = kind then SOME body else NONE |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
134 |
| block_list _ _ _ = NONE; |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
135 |
|
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
136 |
val is_list = fn List _ => true | _ => false; |
61452 | 137 |
|
138 |
||
139 |
(* read document *) |
|
140 |
||
141 |
local |
|
61450 | 142 |
|
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
143 |
fun build (indent, item, rev_body) document = |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
144 |
(case (item, document) of |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
145 |
(SOME kind, block :: blocks) => |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
146 |
(case block_list indent kind block of |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
147 |
SOME list => List {indent = indent, kind = kind, body = fold cons rev_body list} :: blocks |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
148 |
| NONE => |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
149 |
if (if is_list block then indent < block_indent block else indent <= block_indent block) |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
150 |
then build (indent, item, block :: rev_body) blocks |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
151 |
else List {indent = indent, kind = kind, body = rev rev_body} :: document) |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
152 |
| (SOME kind, []) => [List {indent = indent, kind = kind, body = rev rev_body}] |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
153 |
| (NONE, _) => fold cons rev_body document); |
61445 | 154 |
|
61460 | 155 |
fun plain_line (line as Line {is_empty, item, ...}) = |
156 |
not is_empty andalso is_none item andalso line <> eof_line; |
|
61444 | 157 |
|
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
158 |
val parse_paragraph = |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
159 |
Scan.one (fn line => line <> eof_line) -- Scan.many plain_line >> (fn (line, lines) => |
61460 | 160 |
let |
161 |
val Line {indent, item, ...} = line; |
|
162 |
val block = Paragraph (line :: lines); |
|
163 |
in (indent, item, [block]) end); |
|
61443 | 164 |
|
165 |
val parse_document = |
|
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
166 |
parse_paragraph ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_paragraph) |
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
167 |
>> (fn pars => fold_rev build pars []); |
61441 | 168 |
|
169 |
in |
|
170 |
||
61445 | 171 |
val read_lines = |
172 |
Scan.read (Scan.stopper (K eof_line) (fn line => line = eof_line)) |
|
173 |
(Scan.repeat (Scan.many line_is_empty |-- parse_document) --| Scan.many line_is_empty) #> |
|
174 |
the_default [] #> flat; |
|
61441 | 175 |
|
61457 | 176 |
val read_antiquotes = Antiquote.split_lines #> map make_line #> read_lines; |
177 |
val read_source = Antiquote.read #> read_antiquotes; |
|
61441 | 178 |
|
61457 | 179 |
end; |
61445 | 180 |
|
61449 | 181 |
|
182 |
(* PIDE reports *) |
|
183 |
||
61457 | 184 |
val text_reports = |
185 |
maps (fn Antiquote.Text ss => [(#1 (Symbol_Pos.range ss), Markup.words)] | _ => []); |
|
186 |
||
61449 | 187 |
local |
188 |
||
61460 | 189 |
fun line_reports depth (Line {item_pos, content, ...}) = |
190 |
cons (item_pos, Markup.markdown_item depth) #> append (text_reports content); |
|
61449 | 191 |
|
61452 | 192 |
fun block_reports depth block = |
193 |
(case block of |
|
194 |
Paragraph lines => |
|
195 |
cons (#1 (block_range block), Markup.markdown_paragraph) #> |
|
61450 | 196 |
fold (line_reports depth) lines |
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61457
diff
changeset
|
197 |
| List {kind, body, ...} => |
61452 | 198 |
cons (#1 (block_range block), Markup.markdown_list (print_kind kind)) #> |
199 |
fold (block_reports (depth + 1)) body); |
|
61449 | 200 |
|
201 |
in |
|
202 |
||
61450 | 203 |
fun reports blocks = |
204 |
filter (Position.is_reported o #1) (fold (block_reports 0) blocks []); |
|
61449 | 205 |
|
61441 | 206 |
end; |
61449 | 207 |
|
208 |
end; |