1.1 --- a/src/Pure/System/options.scala	Fri Jul 20 22:39:59 2012 +0200
     1.2 +++ b/src/Pure/System/options.scala	Fri Jul 20 23:16:54 2012 +0200
     1.3 @@ -51,8 +51,7 @@
     1.4  
     1.5      def parse_entries(file: JFile): List[Options => Options] =
     1.6      {
     1.7 -      val toks = syntax.scan(Standard_System.read_file(file))
     1.8 -      parse_all(rep(entry), Token.reader(toks, file.toString)) match {
     1.9 +      parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.toString)) match {
    1.10          case Success(result, _) => result
    1.11          case bad => error(bad.toString)
    1.12        }