equal
deleted
inserted
replaced
192 fun !!! text scan = |
192 fun !!! text scan = |
193 let |
193 let |
194 fun get_pos [] = " (past end-of-text!)" |
194 fun get_pos [] = " (past end-of-text!)" |
195 | get_pos ((_, pos) :: _) = Position.str_of pos; |
195 | get_pos ((_, pos) :: _) = Position.str_of pos; |
196 |
196 |
197 fun err (syms, msg) = |
197 fun err (syms, msg) = fn () => |
198 text ^ get_pos syms ^ " at " ^ beginning 10 (map symbol syms) ^ |
198 text ^ get_pos syms ^ " at " ^ beginning 10 (map symbol syms) ^ |
199 (case msg of NONE => "" | SOME s => "\n" ^ s); |
199 (case msg of NONE => "" | SOME m => "\n" ^ m ()); |
200 in Scan.!! err scan end; |
200 in Scan.!! err scan end; |
201 |
201 |
202 val any_line' = |
202 val any_line' = |
203 Scan.many (not o (Scan.is_stopper char_stopper orf (is_newline o symbol))); |
203 Scan.many (not o (Scan.is_stopper char_stopper orf (is_newline o symbol))); |
204 |
204 |