equal
deleted
inserted
replaced
402 |
402 |
403 (* scanning through symbols *) |
403 (* scanning through symbols *) |
404 |
404 |
405 fun scanner msg scan chs = |
405 fun scanner msg scan chs = |
406 let |
406 let |
407 fun message (cs, NONE) = msg ^ ": " ^ quote (beginning 10 cs) |
407 fun message (cs, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 cs)) |
408 | message (cs, SOME msg') = msg ^ ", " ^ msg' ^ ": " ^ quote (beginning 10 cs); |
408 | message (cs, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 cs)); |
409 val fin_scan = Scan.error (Scan.finite stopper (!! message scan)); |
409 val fin_scan = Scan.error (Scan.finite stopper (!! message scan)); |
410 in |
410 in |
411 (case fin_scan chs of |
411 (case fin_scan chs of |
412 (result, []) => result |
412 (result, []) => result |
413 | (_, rest) => error (message (rest, NONE))) |
413 | (_, rest) => error (message (rest, NONE) ())) |
414 end; |
414 end; |
415 |
415 |
416 val scan_id = Scan.one is_letter ^^ (Scan.many is_letdig >> implode); |
416 val scan_id = Scan.one is_letter ^^ (Scan.many is_letdig >> implode); |
417 |
417 |
418 |
418 |