src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Sat Jul 02 23:04:19 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Sat Jul 02 23:31:07 2011 +0200
@@ -9,7 +9,7 @@
 
 import scala.annotation.tailrec
 import scala.collection.mutable
-import scala.util.parsing.input.Reader
+import scala.util.parsing.input.{Reader, CharSequenceReader}
 import scala.util.matching.Regex
 
 import java.io.File
@@ -99,6 +99,9 @@
     }
   }
 
+  def read(source: CharSequence): Header =
+    read(new CharSequenceReader(source))
+
   def read(file: File): Header =
   {
     val reader = Scan.byte_reader(file)