equal
deleted
inserted
replaced
298 |
298 |
299 (* scan token *) |
299 (* scan token *) |
300 |
300 |
301 fun scan (lex1, lex2) = |
301 fun scan (lex1, lex2) = |
302 let |
302 let |
303 val scanner = Scan.state :-- (fn pos => |
303 val scanner = Scan.state :|-- (fn pos => |
304 let |
304 let |
305 fun token k x = Token (pos, (k, x)); |
305 fun token k x = Token (pos, (k, x)); |
306 fun sync _ = token Sync Symbol.sync; |
306 fun sync _ = token Sync Symbol.sync; |
307 in |
307 in |
308 scan_string >> token String || |
308 scan_string >> token String || |
321 Syntax.scan_var >> token Var || |
321 Syntax.scan_var >> token Var || |
322 Syntax.scan_tid >> token TypeIdent || |
322 Syntax.scan_tid >> token TypeIdent || |
323 Syntax.scan_tvar >> token TypeVar || |
323 Syntax.scan_tvar >> token TypeVar || |
324 Syntax.scan_nat >> token Nat || |
324 Syntax.scan_nat >> token Nat || |
325 scan_symid >> token SymIdent)) |
325 scan_symid >> token SymIdent)) |
326 end) >> #2; |
326 end); |
327 in !! (lex_err (fn cs => "bad input " ^ quote (Symbol.beginning 10 cs))) scanner end; |
327 in !! (lex_err (fn cs => "bad input " ^ quote (Symbol.beginning 10 cs))) scanner end; |
328 |
328 |
329 |
329 |
330 (* token sources *) |
330 (* token sources *) |
331 |
331 |
332 local |
332 local |
333 |
333 |
334 val is_junk = (not o Symbol.is_blank) andf Symbol.is_regular; |
334 val is_junk = (not o Symbol.is_blank) andf Symbol.is_regular; |
335 |
335 |
336 fun recover msg = Scan.state :-- (fn pos => |
336 fun recover msg = Scan.state :|-- (fn pos => |
337 keep_line (Scan.many is_junk) >> (fn xs => [Token (pos, (Error msg, implode xs))])) >> #2; |
337 keep_line (Scan.many is_junk) >> (fn xs => [Token (pos, (Error msg, implode xs))])); |
338 |
338 |
339 in |
339 in |
340 |
340 |
341 fun source do_recover get_lex pos src = |
341 fun source do_recover get_lex pos src = |
342 Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs)) |
342 Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs)) |