src/Pure/General/scan.scala
changeset 48409 0d2114eb412a
parent 48342 4a8f06cbf8bb
child 48743 a72f8ffecf31
equal deleted inserted replaced
48374:623607c5a40f 48409:0d2114eb412a
    10 import scala.collection.{IndexedSeq, TraversableOnce}
    10 import scala.collection.{IndexedSeq, TraversableOnce}
    11 import scala.collection.immutable.PagedSeq
    11 import scala.collection.immutable.PagedSeq
    12 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
    12 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
    13 import scala.util.parsing.combinator.RegexParsers
    13 import scala.util.parsing.combinator.RegexParsers
    14 
    14 
    15 import java.io.{File, BufferedInputStream, FileInputStream}
    15 import java.io.{File => JFile, BufferedInputStream, FileInputStream}
    16 
    16 
    17 
    17 
    18 object Scan
    18 object Scan
    19 {
    19 {
    20   /** context of partial scans **/
    20   /** context of partial scans **/
   420     }
   420     }
   421   }
   421   }
   422 
   422 
   423   abstract class Byte_Reader extends Reader[Char] { def close: Unit }
   423   abstract class Byte_Reader extends Reader[Char] { def close: Unit }
   424 
   424 
   425   def byte_reader(file: File): Byte_Reader =
   425   def byte_reader(file: JFile): Byte_Reader =
   426   {
   426   {
   427     val stream = new BufferedInputStream(new FileInputStream(file))
   427     val stream = new BufferedInputStream(new FileInputStream(file))
   428     val seq = new PagedSeq(
   428     val seq = new PagedSeq(
   429       (buf: Array[Char], offset: Int, length: Int) =>
   429       (buf: Array[Char], offset: Int, length: Int) =>
   430         {
   430         {