src/Pure/Thy/thy_header.scala
changeset 59695 a03e0561bdbf
parent 59694 d2bb4b5ed862
child 59705 740a0ca7e09b
     1.1 --- a/src/Pure/Thy/thy_header.scala	Sat Mar 14 18:18:40 2015 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Mar 14 19:51:36 2015 +0100
     1.3 @@ -124,7 +124,7 @@
     1.4  
     1.5    /* read -- lazy scanning */
     1.6  
     1.7 -  def read(reader: Reader[Char]): Thy_Header =
     1.8 +  def read(reader: Reader[Char], file: String): Thy_Header =
     1.9    {
    1.10      val token = Token.Parsers.token(bootstrap_keywords)
    1.11      val toks = new mutable.ListBuffer[Token]
    1.12 @@ -140,14 +140,14 @@
    1.13      }
    1.14      scan_to_begin(reader)
    1.15  
    1.16 -    parse(commit(header), Token.reader(toks.toList)) match {
    1.17 +    parse(commit(header), Token.reader(toks.toList, file)) match {
    1.18        case Success(result, _) => result
    1.19        case bad => error(bad.toString)
    1.20      }
    1.21    }
    1.22  
    1.23 -  def read(source: CharSequence): Thy_Header =
    1.24 -    read(new CharSequenceReader(source))
    1.25 +  def read(source: CharSequence, file: String): Thy_Header =
    1.26 +    read(new CharSequenceReader(source), file)
    1.27  }
    1.28  
    1.29