61441
|
1 |
(* Title: Pure/Thy/markdown.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Minimal support for Markdown documents (see also http://commonmark.org).
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature MARKDOWN =
|
|
8 |
sig
|
|
9 |
type line
|
|
10 |
val read: Input.source -> line list list
|
|
11 |
end;
|
|
12 |
|
|
13 |
structure Markdown: MARKDOWN =
|
|
14 |
struct
|
|
15 |
|
|
16 |
(* line with optional item marker *)
|
|
17 |
|
|
18 |
datatype kind = Itemize | Enumerate | Description;
|
|
19 |
|
|
20 |
datatype line =
|
|
21 |
Line of
|
|
22 |
{content: Antiquote.text_antiquote list,
|
|
23 |
is_empty: bool,
|
|
24 |
indent: int,
|
|
25 |
marker: (kind * Position.T) option};
|
|
26 |
|
|
27 |
fun line_content (Line {content, ...}) = content;
|
|
28 |
fun line_is_empty (Line {is_empty, ...}) = is_empty;
|
|
29 |
fun line_indent (Line {indent, ...}) = indent;
|
|
30 |
fun line_marker (Line {marker, ...}) = marker;
|
|
31 |
|
|
32 |
local
|
|
33 |
|
|
34 |
fun bad_blank ((s, _): Symbol_Pos.T) = Symbol.is_ascii_blank s andalso s <> Symbol.space;
|
|
35 |
val bad_blanks = maps (fn Antiquote.Text ss => filter bad_blank ss | _ => []);
|
|
36 |
|
|
37 |
fun check_blanks content =
|
|
38 |
(case bad_blanks content of
|
|
39 |
[] => ()
|
|
40 |
| (c, pos) :: _ =>
|
|
41 |
error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos));
|
|
42 |
|
|
43 |
fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space;
|
|
44 |
val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
|
|
45 |
|
|
46 |
fun line_kind (Antiquote.Text ss :: _) =
|
|
47 |
let
|
|
48 |
val (spaces, rest) = take_prefix is_space ss;
|
|
49 |
fun make_marker kind =
|
|
50 |
(case rest of
|
|
51 |
[(_, pos)] => (kind, pos)
|
|
52 |
| (_, pos) :: (" ", _) :: _ => (kind, pos)
|
|
53 |
| (_, pos) :: _ => error ("Missing space after item marker" ^ Position.here pos));
|
|
54 |
val marker =
|
|
55 |
(case rest of
|
|
56 |
("\<^item>", _) :: _ => SOME (make_marker Itemize)
|
|
57 |
| ("\<^enum>", _) :: _ => SOME (make_marker Enumerate)
|
|
58 |
| ("\<^descr>", _) :: _ => SOME (make_marker Description)
|
|
59 |
| _ => NONE);
|
|
60 |
in (length spaces, marker) end
|
|
61 |
| line_kind _ = (0, NONE);
|
|
62 |
|
|
63 |
in
|
|
64 |
|
|
65 |
fun make_line content =
|
|
66 |
let
|
|
67 |
val _ = check_blanks content;
|
|
68 |
val (indent, marker) = line_kind content;
|
|
69 |
in Line {content = content, is_empty = is_empty content, indent = indent, marker = marker} end;
|
|
70 |
|
|
71 |
end;
|
|
72 |
|
|
73 |
|
|
74 |
(* spans of related lines *)
|
|
75 |
|
|
76 |
local
|
|
77 |
|
|
78 |
val eof = make_line [Antiquote.Text [(Symbol.eof, Position.none)]];
|
|
79 |
val stopper = Scan.stopper (K eof) (fn line => line = eof);
|
|
80 |
|
|
81 |
fun item_line line = is_some (line_marker line);
|
|
82 |
fun plain_line line = is_none (line_marker line) andalso line <> eof;
|
|
83 |
|
|
84 |
val parse_span =
|
|
85 |
Scan.one item_line -- Scan.many plain_line >> op :: ||
|
|
86 |
Scan.many1 plain_line ||
|
|
87 |
Scan.many1 line_is_empty;
|
|
88 |
|
|
89 |
in
|
|
90 |
|
|
91 |
fun read_spans lines =
|
|
92 |
the_default [] (Scan.read stopper (Scan.repeat parse_span) lines);
|
|
93 |
|
|
94 |
end;
|
|
95 |
|
|
96 |
|
|
97 |
(* document structure *)
|
|
98 |
|
|
99 |
fun read input =
|
|
100 |
Antiquote.read input
|
|
101 |
|> Antiquote.split_lines
|
|
102 |
|> map make_line
|
|
103 |
|> read_spans;
|
|
104 |
|
|
105 |
end;
|