# HG changeset patch
# User wenzelm
# Date 1309642267 -7200
# Node ID 598b2c6ce13f51a36fbf20eae3b084d532df73e8
# Parent  ac886d096c11b8dcb7e79b5faa9eed8e2881e869
Thy_Header.read convenience;

diff -r ac886d096c11 -r 598b2c6ce13f 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)