--- a/src/Pure/Thy/thy_header.scala Sat Jan 07 19:36:40 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala Sat Jan 07 20:01:05 2017 +0100
@@ -9,7 +9,7 @@
import scala.annotation.tailrec
import scala.collection.mutable
-import scala.util.parsing.input.{Reader, CharSequenceReader}
+import scala.util.parsing.input.Reader
import scala.util.matching.Regex
@@ -176,9 +176,6 @@
}
}
- def read(source: CharSequence, start: Token.Pos): Thy_Header =
- read(new CharSequenceReader(source), start)
-
/* line-oriented text */