src/Pure/Tools/build.scala
changeset 59705 740a0ca7e09b
parent 59692 03aa1b63af10
child 59723 193f12622072
     1.1 --- a/src/Pure/Tools/build.scala	Sun Mar 15 19:48:49 2015 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Sun Mar 15 20:35:47 2015 +0100
     1.3 @@ -260,8 +260,9 @@
     1.4      def parse_entries(root: Path): List[(String, Session_Entry)] =
     1.5      {
     1.6        val toks = Token.explode(root_syntax.keywords, File.read(root))
     1.7 +      val start = Token.Pos.file(root.implode)
     1.8  
     1.9 -      parse_all(rep(chapter | session_entry), Token.reader(toks, root.implode)) match {
    1.10 +      parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
    1.11          case Success(result, _) =>
    1.12            var chapter = chapter_default
    1.13            val entries = new mutable.ListBuffer[(String, Session_Entry)]