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