# HG changeset patch
# User wenzelm
# Date 1345747740 -7200
# Node ID 51560e392e1b2c8c5a1d2fe31fadc948457c93bf
# Parent  f686cb016c0cef153c1a118852f82962434d6605
eliminated obsolete byte_reader -- theory headers + body files are parsed in full;

diff -r f686cb016c0c -r 51560e392e1b src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Thu Aug 23 20:34:51 2012 +0200
+++ b/src/Pure/General/scan.scala	Thu Aug 23 20:49:00 2012 +0200
@@ -400,62 +400,4 @@
       string | (alt_string | (verb | (cmt | other)))
     }
   }
-
-
-
-  /** read file without decoding -- enables efficient length operation **/
-
-  private class Restricted_Seq(seq: IndexedSeq[Char], start: Int, end: Int)
-    extends CharSequence
-  {
-    def charAt(i: Int): Char =
-      if (0 <= i && i < length) seq(start + i)
-      else throw new IndexOutOfBoundsException
-
-    def length: Int = end - start  // avoid potentially expensive seq.length
-
-    def subSequence(i: Int, j: Int): CharSequence =
-      if (0 <= i && i <= j && j <= length) new Restricted_Seq(seq, start + i, start + j)
-      else throw new IndexOutOfBoundsException
-
-    override def toString: String =
-    {
-      val buf = new StringBuilder(length)
-      for (offset <- start until end) buf.append(seq(offset))
-      buf.toString
-    }
-  }
-
-  abstract class Byte_Reader extends Reader[Char] { def close: Unit }
-
-  def byte_reader(file: JFile): Byte_Reader =
-  {
-    val stream = new BufferedInputStream(new FileInputStream(file))
-    val seq = new PagedSeq(
-      (buf: Array[Char], offset: Int, length: Int) =>
-        {
-          var i = 0
-          var c = 0
-          var eof = false
-          while (!eof && i < length) {
-            c = stream.read
-            if (c == -1) eof = true
-            else { buf(offset + i) = c.toChar; i += 1 }
-          }
-          if (i > 0) i else -1
-        })
-    val restricted_seq = new Restricted_Seq(seq, 0, file.length.toInt)
-
-    class Paged_Reader(override val offset: Int) extends Byte_Reader
-    {
-      override lazy val source: CharSequence = restricted_seq
-      def first: Char = if (seq.isDefinedAt(offset)) seq(offset) else '\032'
-      def rest: Paged_Reader = if (seq.isDefinedAt(offset)) new Paged_Reader(offset + 1) else this
-      def pos: InputPosition = new OffsetPosition(source, offset)
-      def atEnd: Boolean = !seq.isDefinedAt(offset)
-      override def drop(n: Int): Paged_Reader = new Paged_Reader(offset + n)
-      def close { stream.close }
-    }
-    new Paged_Reader(0)
-  }
 }