changeset 59083 | 88b0b1f28adc |
parent 58928 | 23d0ffd48006 |
child 59136 | c2b23cb8a677 |
--- a/src/Pure/Tools/build.scala Wed Dec 03 11:50:58 2014 +0100 +++ b/src/Pure/Tools/build.scala Wed Dec 03 14:04:38 2014 +0100 @@ -259,7 +259,7 @@ def parse_entries(root: Path): List[(String, Session_Entry)] = { - val toks = root_syntax.scan(File.read(root)) + val toks = Token.explode(root_syntax.keywords, File.read(root)) parse_all(rep(chapter | session_entry), Token.reader(toks, root.implode)) match { case Success(result, _) =>