equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 signature ANTIQUOTE = |
8 signature ANTIQUOTE = |
9 sig |
9 sig |
10 datatype antiquote = |
10 datatype antiquote = |
11 Text of string | Antiq of SymbolPos.text * Position.T | |
11 Text of string | Antiq of SymbolPos.T list * Position.T | |
12 Open of Position.T | Close of Position.T |
12 Open of Position.T | Close of Position.T |
13 val is_antiq: antiquote -> bool |
13 val is_antiq: antiquote -> bool |
14 val read: SymbolPos.text * Position.T -> antiquote list |
14 val read: SymbolPos.T list * Position.T -> antiquote list |
15 val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) -> |
15 val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) -> |
16 SymbolPos.text * Position.T -> 'a |
16 SymbolPos.T list * Position.T -> 'a |
17 end; |
17 end; |
18 |
18 |
19 structure Antiquote: ANTIQUOTE = |
19 structure Antiquote: ANTIQUOTE = |
20 struct |
20 struct |
21 |
21 |
22 (* datatype antiquote *) |
22 (* datatype antiquote *) |
23 |
23 |
24 datatype antiquote = |
24 datatype antiquote = |
25 Text of string | |
25 Text of string | |
26 Antiq of string * Position.T | |
26 Antiq of SymbolPos.T list * Position.T | |
27 Open of Position.T | |
27 Open of Position.T | |
28 Close of Position.T; |
28 Close of Position.T; |
29 |
29 |
30 fun is_antiq (Text _) = false |
30 fun is_antiq (Text _) = false |
31 | is_antiq _ = true; |
31 | is_antiq _ = true; |
65 |
65 |
66 val scan_antiq = |
66 val scan_antiq = |
67 SymbolPos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- |
67 SymbolPos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- |
68 T.!!! "missing closing brace of antiquotation" |
68 T.!!! "missing closing brace of antiquotation" |
69 (Scan.repeat scan_ant -- ($$$ "}" |-- SymbolPos.scan_pos))) |
69 (Scan.repeat scan_ant -- ($$$ "}" |-- SymbolPos.scan_pos))) |
70 >> (fn (pos1, (body, pos2)) => |
70 >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2))); |
71 let val (s, (pos, _)) = SymbolPos.implode_range pos1 pos2 (flat body) |
|
72 in Antiq (s, pos) end); |
|
73 |
71 |
74 in |
72 in |
75 |
73 |
76 val scan_antiquote = |
74 val scan_antiquote = |
77 (Scan.repeat1 scan_txt >> (Text o SymbolPos.content o flat) || |
75 (Scan.repeat1 scan_txt >> (Text o SymbolPos.content o flat) || |
82 end; |
80 end; |
83 |
81 |
84 |
82 |
85 (* read *) |
83 (* read *) |
86 |
84 |
87 fun read ("", _) = [] |
85 fun read ([], _) = [] |
88 | read (s, pos) = |
86 | read (syms, pos) = |
89 (case Scan.read SymbolPos.stopper (Scan.repeat scan_antiquote) (SymbolPos.explode (s, pos)) of |
87 (case Scan.read SymbolPos.stopper (Scan.repeat scan_antiquote) syms of |
90 SOME xs => (check_nesting xs; xs) |
88 SOME xs => (check_nesting xs; xs) |
91 | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos)); |
89 | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos)); |
92 |
90 |
93 |
91 |
94 (* read_antiq *) |
92 (* read_antiq *) |
95 |
93 |
96 fun read_antiq lex scan (s, pos) = |
94 fun read_antiq lex scan (syms, pos) = |
97 let |
95 let |
98 fun err msg = cat_error msg |
96 fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^ |
99 ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos); |
97 "@{" ^ SymbolPos.content syms ^ "}"); |
100 |
98 |
101 val res = |
99 val res = |
102 Source.of_list (SymbolPos.explode (s, pos)) |
100 Source.of_list syms |
103 |> T.source' {do_recover = NONE} (K (lex, Scan.empty_lexicon)) |
101 |> T.source' {do_recover = NONE} (K (lex, Scan.empty_lexicon)) |
104 |> T.source_proper |
102 |> T.source_proper |
105 |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE |
103 |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE |
106 |> Source.exhaust; |
104 |> Source.exhaust; |
107 in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end; |
105 in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end; |