equal
deleted
inserted
replaced
49 { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) } |
49 { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) } |
50 } |
50 } |
51 |
51 |
52 def parse_entries(file: JFile): List[Options => Options] = |
52 def parse_entries(file: JFile): List[Options => Options] = |
53 { |
53 { |
54 val toks = syntax.scan(Standard_System.read_file(file)) |
54 parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.toString)) match { |
55 parse_all(rep(entry), Token.reader(toks, file.toString)) match { |
|
56 case Success(result, _) => result |
55 case Success(result, _) => result |
57 case bad => error(bad.toString) |
56 case bad => error(bad.toString) |
58 } |
57 } |
59 } |
58 } |
60 } |
59 } |