src/Pure/System/options.scala
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