6 |
6 |
7 signature ANTIQUOTE = |
7 signature ANTIQUOTE = |
8 sig |
8 sig |
9 type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range} |
9 type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range} |
10 datatype 'a antiquote = Text of 'a | Antiq of antiq |
10 datatype 'a antiquote = Text of 'a | Antiq of antiq |
|
11 type text_antiquote = Symbol_Pos.T list antiquote |
|
12 val split_lines: text_antiquote list -> text_antiquote list list |
11 val antiq_reports: antiq -> Position.report list |
13 val antiq_reports: antiq -> Position.report list |
12 val antiquote_reports: ('a -> Position.report_text list) -> |
14 val antiquote_reports: ('a -> Position.report_text list) -> |
13 'a antiquote list -> Position.report_text list |
15 'a antiquote list -> Position.report_text list |
14 val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list |
16 val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list |
15 val scan_antiquote: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list |
17 val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list |
16 val read: Input.source -> Symbol_Pos.T list antiquote list |
18 val read: Input.source -> text_antiquote list |
17 end; |
19 end; |
18 |
20 |
19 structure Antiquote: ANTIQUOTE = |
21 structure Antiquote: ANTIQUOTE = |
20 struct |
22 struct |
21 |
23 |
22 (* datatype antiquote *) |
24 (* datatype antiquote *) |
23 |
25 |
24 type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}; |
26 type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}; |
25 datatype 'a antiquote = Text of 'a | Antiq of antiq; |
27 datatype 'a antiquote = Text of 'a | Antiq of antiq; |
|
28 |
|
29 type text_antiquote = Symbol_Pos.T list antiquote; |
|
30 |
|
31 |
|
32 (* split lines *) |
|
33 |
|
34 fun split_lines input = |
|
35 let |
|
36 fun add a (line, lines) = (a :: line, lines); |
|
37 fun flush (line, lines) = ([], rev line :: lines); |
|
38 fun split (a as Text ss) = |
|
39 (case take_prefix (fn ("\n", _) => false | _ => true) ss of |
|
40 ([], []) => I |
|
41 | (_, []) => add a |
|
42 | ([], _ :: rest) => flush #> split (Text rest) |
|
43 | (prefix, _ :: rest) => add (Text prefix) #> flush #> split (Text rest)) |
|
44 | split a = add a; |
|
45 in rev (#2 (flush (fold split input ([], [])))) end; |
26 |
46 |
27 |
47 |
28 (* reports *) |
48 (* reports *) |
29 |
49 |
30 fun antiq_reports ((_, {start, stop, range = (pos, _)}): antiq) = |
50 fun antiq_reports ((_, {start, stop, range = (pos, _)}): antiq) = |