src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Sun Mar 15 19:48:49 2015 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Mar 15 20:35:47 2015 +0100
@@ -124,7 +124,7 @@
 
   /* read -- lazy scanning */
 
-  def read(reader: Reader[Char], file: String): Thy_Header =
+  def read(reader: Reader[Char], start: Token.Pos): Thy_Header =
   {
     val token = Token.Parsers.token(bootstrap_keywords)
     val toks = new mutable.ListBuffer[Token]
@@ -140,14 +140,14 @@
     }
     scan_to_begin(reader)
 
-    parse(commit(header), Token.reader(toks.toList, file)) match {
+    parse(commit(header), Token.reader(toks.toList, start)) match {
       case Success(result, _) => result
       case bad => error(bad.toString)
     }
   }
 
-  def read(source: CharSequence, file: String): Thy_Header =
-    read(new CharSequenceReader(source), file)
+  def read(source: CharSequence, start: Token.Pos): Thy_Header =
+    read(new CharSequenceReader(source), start)
 }