# 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)