author | wenzelm |
Thu, 29 Nov 2012 10:45:25 +0100 | |
changeset 50280 | 0eb9b5d09f31 |
parent 50201 | c26369c9eda6 |
child 53167 | 4e7ddd76e632 |
permissions | -rw-r--r-- |
24579 | 1 |
(* Title: Pure/ML/ml_lex.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Lexical syntax for SML. |
|
5 |
*) |
|
6 |
||
7 |
signature ML_LEX = |
|
8 |
sig |
|
9 |
datatype token_kind = |
|
24596 | 10 |
Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String | |
24579 | 11 |
Space | Comment | Error of string | EOF |
12 |
eqtype token |
|
27732 | 13 |
val stopper: token Scan.stopper |
24596 | 14 |
val is_regular: token -> bool |
15 |
val is_improper: token -> bool |
|
30683
e8ac1f9d9469
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents:
30645
diff
changeset
|
16 |
val set_range: Position.range -> token -> token |
30636 | 17 |
val pos_of: token -> Position.T |
31474 | 18 |
val end_pos_of: token -> Position.T |
24579 | 19 |
val kind_of: token -> token_kind |
27817 | 20 |
val content_of: token -> string |
31426 | 21 |
val check_content_of: token -> string |
31332 | 22 |
val flatten: token list -> string |
24579 | 23 |
val keywords: string list |
24596 | 24 |
val source: (Symbol.symbol, 'a) Source.source -> |
30573 | 25 |
(token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) |
27772 | 26 |
Source.source) Source.source |
30591 | 27 |
val tokenize: string -> token list |
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37195
diff
changeset
|
28 |
val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list |
24579 | 29 |
end; |
30 |
||
31 |
structure ML_Lex: ML_LEX = |
|
32 |
struct |
|
33 |
||
34 |
(** tokens **) |
|
35 |
||
36 |
(* datatype token *) |
|
37 |
||
38 |
datatype token_kind = |
|
24596 | 39 |
Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String | |
24579 | 40 |
Space | Comment | Error of string | EOF; |
41 |
||
27772 | 42 |
datatype token = Token of Position.range * (token_kind * string); |
43 |
||
44 |
||
45 |
(* position *) |
|
46 |
||
30683
e8ac1f9d9469
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents:
30645
diff
changeset
|
47 |
fun set_range range (Token (_, x)) = Token (range, x); |
e8ac1f9d9469
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents:
30645
diff
changeset
|
48 |
|
30636 | 49 |
fun pos_of (Token ((pos, _), _)) = pos; |
50 |
fun end_pos_of (Token ((_, pos), _)) = pos; |
|
24579 | 51 |
|
52 |
||
24596 | 53 |
(* control tokens *) |
24579 | 54 |
|
27772 | 55 |
fun mk_eof pos = Token ((pos, Position.none), (EOF, "")); |
56 |
val eof = mk_eof Position.none; |
|
24579 | 57 |
|
58 |
fun is_eof (Token (_, (EOF, _))) = true |
|
59 |
| is_eof _ = false; |
|
60 |
||
27772 | 61 |
val stopper = |
30636 | 62 |
Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; |
27772 | 63 |
|
24579 | 64 |
|
27772 | 65 |
(* token content *) |
66 |
||
31426 | 67 |
fun kind_of (Token (_, (k, _))) = k; |
68 |
||
27817 | 69 |
fun content_of (Token (_, (_, x))) = x; |
70 |
fun token_leq (tok, tok') = content_of tok <= content_of tok'; |
|
27772 | 71 |
|
41502
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
72 |
fun is_regular (Token (_, (Error _, _))) = false |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
73 |
| is_regular (Token (_, (EOF, _))) = false |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
74 |
| is_regular _ = true; |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
75 |
|
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
76 |
fun is_improper (Token (_, (Space, _))) = true |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
77 |
| is_improper (Token (_, (Comment, _))) = true |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
78 |
| is_improper _ = false; |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
79 |
|
40337
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
80 |
fun warn tok = |
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
81 |
(case tok of |
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
82 |
Token (_, (Keyword, ":>")) => |
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
83 |
warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\ |
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
84 |
\prefer non-opaque matching (:) possibly with abstype" ^ |
48992 | 85 |
Position.here (pos_of tok)) |
40337
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
86 |
| _ => ()); |
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
87 |
|
31426 | 88 |
fun check_content_of tok = |
30636 | 89 |
(case kind_of tok of |
30645 | 90 |
Error msg => error msg |
40337
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
91 |
| _ => content_of tok); |
30636 | 92 |
|
41502
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
93 |
fun flatten_content (tok :: (toks as tok' :: _)) = |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
94 |
Symbol.escape (check_content_of tok) :: |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
95 |
(if is_improper tok orelse is_improper tok' then flatten_content toks |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
96 |
else Symbol.space :: flatten_content toks) |
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
97 |
| flatten_content toks = map (Symbol.escape o check_content_of) toks; |
31332 | 98 |
|
41502
967cbbc77abd
refined ML_Lex.flatten: ensure proper separation of tokens;
wenzelm
parents:
40627
diff
changeset
|
99 |
val flatten = implode o flatten_content; |
24596 | 100 |
|
101 |
||
30614 | 102 |
(* markup *) |
103 |
||
37195 | 104 |
local |
105 |
||
30645 | 106 |
val token_kind_markup = |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
107 |
fn Keyword => (Markup.ML_keyword, "") |
48768
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48756
diff
changeset
|
108 |
| Ident => (Markup.empty, "") |
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48756
diff
changeset
|
109 |
| LongIdent => (Markup.empty, "") |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
110 |
| TypeVar => (Markup.ML_tvar, "") |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
111 |
| Word => (Markup.ML_numeral, "") |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
112 |
| Int => (Markup.ML_numeral, "") |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
113 |
| Real => (Markup.ML_numeral, "") |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
114 |
| Char => (Markup.ML_char, "") |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
115 |
| String => (Markup.ML_string, "") |
48768
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48756
diff
changeset
|
116 |
| Space => (Markup.empty, "") |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
117 |
| Comment => (Markup.ML_comment, "") |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
118 |
| Error msg => (Markup.bad, msg) |
48768
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48756
diff
changeset
|
119 |
| EOF => (Markup.empty, ""); |
30614 | 120 |
|
37195 | 121 |
fun token_markup kind x = |
122 |
if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
123 |
then (Markup.ML_delimiter, "") |
37195 | 124 |
else token_kind_markup kind; |
125 |
||
126 |
in |
|
127 |
||
48768
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48756
diff
changeset
|
128 |
fun report_of_token (Token ((pos, _), (kind, x))) = |
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48756
diff
changeset
|
129 |
let val (markup, txt) = token_markup kind x |
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48756
diff
changeset
|
130 |
in ((pos, markup), txt) end; |
37195 | 131 |
|
132 |
end; |
|
30614 | 133 |
|
134 |
||
24579 | 135 |
|
136 |
(** scanners **) |
|
137 |
||
30573 | 138 |
open Basic_Symbol_Pos; |
24579 | 139 |
|
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
41502
diff
changeset
|
140 |
fun !!! msg = Symbol_Pos.!!! (fn () => "SML lexical error: " ^ msg); |
24579 | 141 |
|
142 |
||
27772 | 143 |
(* blanks *) |
24579 | 144 |
|
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
145 |
val scan_blank = Scan.one (Symbol.is_ascii_blank o Symbol_Pos.symbol); |
27772 | 146 |
val scan_blanks1 = Scan.repeat1 scan_blank; |
24579 | 147 |
|
148 |
||
149 |
(* keywords *) |
|
150 |
||
151 |
val keywords = ["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=", |
|
152 |
"=>", "[", "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as", |
|
153 |
"case", "datatype", "do", "else", "end", "eqtype", "exception", "fn", |
|
154 |
"fun", "functor", "handle", "if", "in", "include", "infix", "infixr", |
|
155 |
"let", "local", "nonfix", "of", "op", "open", "orelse", "raise", "rec", |
|
156 |
"sharing", "sig", "signature", "struct", "structure", "then", "type", |
|
157 |
"val", "where", "while", "with", "withtype"]; |
|
158 |
||
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40525
diff
changeset
|
159 |
val lex = Scan.make_lexicon (map raw_explode keywords); |
27772 | 160 |
fun scan_keyword x = Scan.literal lex x; |
24579 | 161 |
|
162 |
||
163 |
(* identifiers *) |
|
164 |
||
24596 | 165 |
local |
166 |
||
24579 | 167 |
val scan_letdigs = |
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
168 |
Scan.many |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
169 |
((Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf Symbol.is_ascii_quasi) o |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
170 |
Symbol_Pos.symbol); |
24579 | 171 |
|
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
172 |
val scan_alphanumeric = |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
173 |
Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) -- scan_letdigs >> op ::; |
24579 | 174 |
|
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
175 |
val scan_symbolic = |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40525
diff
changeset
|
176 |
Scan.many1 (member (op =) (raw_explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol); |
24579 | 177 |
|
24596 | 178 |
in |
179 |
||
24579 | 180 |
val scan_ident = scan_alphanumeric || scan_symbolic; |
181 |
||
182 |
val scan_longident = |
|
27772 | 183 |
(Scan.repeat1 (scan_alphanumeric @@@ $$$ ".") >> flat) @@@ (scan_ident || $$$ "="); |
24579 | 184 |
|
27772 | 185 |
val scan_typevar = $$$ "'" @@@ scan_letdigs; |
24579 | 186 |
|
24596 | 187 |
end; |
24579 | 188 |
|
189 |
||
190 |
(* numerals *) |
|
191 |
||
24596 | 192 |
local |
193 |
||
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
194 |
val scan_dec = Scan.many1 (Symbol.is_ascii_digit o Symbol_Pos.symbol); |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
195 |
val scan_hex = Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol); |
27772 | 196 |
val scan_sign = Scan.optional ($$$ "~") []; |
197 |
val scan_decint = scan_sign @@@ scan_dec; |
|
24579 | 198 |
|
24596 | 199 |
in |
200 |
||
27772 | 201 |
val scan_word = |
202 |
$$$ "0" @@@ $$$ "w" @@@ $$$ "x" @@@ scan_hex || |
|
203 |
$$$ "0" @@@ $$$ "w" @@@ scan_dec; |
|
24579 | 204 |
|
27772 | 205 |
val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec); |
24579 | 206 |
|
27772 | 207 |
val scan_exp = ($$$ "E" || $$$ "e") @@@ scan_decint; |
24579 | 208 |
|
209 |
val scan_real = |
|
27772 | 210 |
scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] || |
211 |
scan_decint @@@ scan_exp; |
|
24579 | 212 |
|
24596 | 213 |
end; |
214 |
||
24579 | 215 |
|
216 |
(* chars and strings *) |
|
217 |
||
24596 | 218 |
local |
219 |
||
220 |
val scan_escape = |
|
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40525
diff
changeset
|
221 |
Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single || |
27772 | 222 |
$$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) || |
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
223 |
Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
224 |
Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- |
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset
|
225 |
Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]); |
24596 | 226 |
|
227 |
val scan_str = |
|
30600
de241396389c
allow non-printable symbols within string tokens;
wenzelm
parents:
30593
diff
changeset
|
228 |
Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso |
de241396389c
allow non-printable symbols within string tokens;
wenzelm
parents:
30593
diff
changeset
|
229 |
(not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single || |
27772 | 230 |
$$$ "\\" @@@ !!! "bad escape character in string" scan_escape; |
24596 | 231 |
|
27772 | 232 |
val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\"; |
233 |
val scan_gaps = Scan.repeat scan_gap >> flat; |
|
24579 | 234 |
|
24596 | 235 |
in |
24579 | 236 |
|
237 |
val scan_char = |
|
27772 | 238 |
$$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ scan_str @@@ scan_gaps @@@ $$$ "\""; |
24579 | 239 |
|
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
240 |
val recover_char = |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
241 |
$$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ Scan.optional (Scan.permissive scan_str @@@ scan_gaps) []; |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
242 |
|
24579 | 243 |
val scan_string = |
27772 | 244 |
$$$ "\"" @@@ !!! "missing quote at end of string" |
245 |
((Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\""); |
|
24596 | 246 |
|
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
247 |
val recover_string = |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
248 |
$$$ "\"" @@@ (Scan.repeat (scan_gap || Scan.permissive scan_str) >> flat); |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
249 |
|
24596 | 250 |
end; |
24579 | 251 |
|
252 |
||
30645 | 253 |
(* scan tokens *) |
24579 | 254 |
|
255 |
local |
|
256 |
||
30593 | 257 |
fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss)); |
24579 | 258 |
|
30593 | 259 |
val scan_ml = |
27772 | 260 |
(scan_char >> token Char || |
261 |
scan_string >> token String || |
|
262 |
scan_blanks1 >> token Space || |
|
30573 | 263 |
Symbol_Pos.scan_comment !!! >> token Comment || |
27772 | 264 |
Scan.max token_leq |
265 |
(scan_keyword >> token Keyword) |
|
266 |
(scan_word >> token Word || |
|
267 |
scan_real >> token Real || |
|
268 |
scan_int >> token Int || |
|
269 |
scan_longident >> token LongIdent || |
|
270 |
scan_ident >> token Ident || |
|
271 |
scan_typevar >> token TypeVar)); |
|
272 |
||
30645 | 273 |
val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text; |
274 |
||
27772 | 275 |
fun recover msg = |
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
276 |
(recover_char || |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
277 |
recover_string || |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
278 |
Symbol_Pos.recover_comment || |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
279 |
Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) |
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
45666
diff
changeset
|
280 |
>> (single o token (Error msg)); |
24579 | 281 |
|
282 |
in |
|
283 |
||
24596 | 284 |
fun source src = |
30573 | 285 |
Symbol_Pos.source (Position.line 1) src |
30593 | 286 |
|> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover)); |
30591 | 287 |
|
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40337
diff
changeset
|
288 |
val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust; |
24579 | 289 |
|
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37195
diff
changeset
|
290 |
fun read pos txt = |
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37195
diff
changeset
|
291 |
let |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
292 |
val _ = Position.report pos Markup.ML_source; |
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37195
diff
changeset
|
293 |
val syms = Symbol_Pos.explode (txt, pos); |
37209
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
294 |
val termination = |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
295 |
if null syms then [] |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
296 |
else |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
297 |
let |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
298 |
val pos1 = List.last syms |-> Position.advance; |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
299 |
val pos2 = Position.advance Symbol.space pos1; |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
300 |
in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end; |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
301 |
val input = |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
302 |
(Source.of_list syms |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
303 |
|> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq)) |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
304 |
(SOME (false, fn msg => recover msg >> map Antiquote.Text)) |
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
305 |
|> Source.exhaust |
48768
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48756
diff
changeset
|
306 |
|> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token)) |
37209
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
307 |
|> tap Antiquote.check_nesting |
40337
d25bbb5f1c9e
warn in correlation with report -- avoid spurious message duplicates;
wenzelm
parents:
40319
diff
changeset
|
308 |
|> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ()))) |
37209
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
309 |
handle ERROR msg => |
48992 | 310 |
cat_error msg ("The error(s) above occurred in ML source" ^ Position.here pos); |
37209
1c8cf0048934
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents:
37198
diff
changeset
|
311 |
in input @ termination end; |
30645 | 312 |
|
24579 | 313 |
end; |
314 |
||
24596 | 315 |
end; |
24579 | 316 |