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