# HG changeset patch
# User wenzelm
# Date 1399025342 -7200
# Node ID 2e6d46a3a617c9375bbd744f73740d81028134ff
# Parent  7fbed439b8d364e084030a652afbbaa018617aaa
reclaimed Byte_Reader from 51560e392e1b;

diff -r 7fbed439b8d3 -r 2e6d46a3a617 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri May 02 07:54:23 2014 +0200
+++ b/src/Pure/General/scan.scala	Fri May 02 12:09:02 2014 +0200
@@ -408,4 +408,62 @@
       scan_tree(rep, "", 0)
     }
   }
+
+
+
+  /** 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)
+  }
 }