src/Pure/Tools/build.scala
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, _) =>