src/Pure/Thy/thy_scan.ML
changeset 5112 9e74cf11e4a4
parent 4938 c8bbbf3c59fa
child 5910 151ee1a5c09c
equal deleted inserted replaced
5111:8f4b72f0c15d 5112:9e74cf11e4a4
   144     val scan_toks = Scan.repeat (scan_token lex);
   144     val scan_toks = Scan.repeat (scan_token lex);
   145     val ignore = fn (Ignore, _, _) => true | _ => false;
   145     val ignore = fn (Ignore, _, _) => true | _ => false;
   146   in
   146   in
   147     (case Scan.error (Scan.finite' Symbol.stopper scan_toks) (Some 1, chs) of
   147     (case Scan.error (Scan.finite' Symbol.stopper scan_toks) (Some 1, chs) of
   148       (toks, (n, [])) => filter_out ignore toks @ [token EOF n "end-of-file"]
   148       (toks, (n, [])) => filter_out ignore toks @ [token EOF n "end-of-file"]
   149     | (_, (n, cs)) => error (lex_err n ("Bad input " ^ quote (beginning cs))))
   149     | (_, (n, cs)) => error (lex_err n ("Bad input " ^ quote (Symbol.beginning cs))))
   150   end;
   150   end;
   151 
   151 
   152 
   152 
   153 end;
   153 end;