changeset 59083 | 88b0b1f28adc |
parent 58999 | ed09ae4ea2d8 |
child 59692 | 03aa1b63af10 |
--- a/src/Pure/System/options.scala Wed Dec 03 11:50:58 2014 +0100 +++ b/src/Pure/System/options.scala Wed Dec 03 14:04:38 2014 +0100 @@ -108,7 +108,7 @@ def parse_file(syntax: Outer_Syntax, parser: Parser[Options => Options], options: Options, file: Path): Options = { - val toks = syntax.scan(File.read(file)) + val toks = Token.explode(syntax.keywords, File.read(file)) val ops = parse_all(rep(parser), Token.reader(toks, file.implode)) match { case Success(result, _) => result