1.1 --- a/src/Pure/Thy/thy_header.scala	Sat Jul 02 23:04:19 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Jul 02 23:31:07 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  import scala.annotation.tailrec
     1.6  import scala.collection.mutable
     1.7 -import scala.util.parsing.input.Reader
     1.8 +import scala.util.parsing.input.{Reader, CharSequenceReader}
     1.9  import scala.util.matching.Regex
    1.10  
    1.11  import java.io.File
    1.12 @@ -99,6 +99,9 @@
    1.13      }
    1.14    }
    1.15  
    1.16 +  def read(source: CharSequence): Header =
    1.17 +    read(new CharSequenceReader(source))
    1.18 +
    1.19    def read(file: File): Header =
    1.20    {
    1.21      val reader = Scan.byte_reader(file)