# HG changeset patch
# User wenzelm
# Date 1399026460 -7200
# Node ID 6101243e6740fdf72e83b7743923531072859656
# Parent  2e6d46a3a617c9375bbd744f73740d81028134ff
support URLs as well;

diff -r 2e6d46a3a617 -r 6101243e6740 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri May 02 12:09:02 2014 +0200
+++ b/src/Pure/General/scan.scala	Fri May 02 12:27:40 2014 +0200
@@ -13,7 +13,8 @@
 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
 import scala.util.parsing.combinator.RegexParsers
 
-import java.io.{File => JFile, BufferedInputStream, FileInputStream}
+import java.io.{File => JFile, BufferedInputStream, FileInputStream, InputStream}
+import java.net.URL
 
 
 object Scan
@@ -411,7 +412,7 @@
 
 
 
-  /** read file without decoding -- enables efficient length operation **/
+  /** read stream without decoding: efficient length operation **/
 
   private class Restricted_Seq(seq: IndexedSeq[Char], start: Int, end: Int)
     extends CharSequence
@@ -420,7 +421,7 @@
       if (0 <= i && i < length) seq(start + i)
       else throw new IndexOutOfBoundsException
 
-    def length: Int = end - start  // avoid potentially expensive seq.length
+    def length: Int = end - start  // avoid 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)
@@ -436,9 +437,9 @@
 
   abstract class Byte_Reader extends Reader[Char] { def close: Unit }
 
-  def byte_reader(file: JFile): Byte_Reader =
+  private def make_byte_reader(stream: InputStream, stream_length: Int): Byte_Reader =
   {
-    val stream = new BufferedInputStream(new FileInputStream(file))
+    val buffered_stream = new BufferedInputStream(stream)
     val seq = new PagedSeq(
       (buf: Array[Char], offset: Int, length: Int) =>
         {
@@ -446,13 +447,13 @@
           var c = 0
           var eof = false
           while (!eof && i < length) {
-            c = stream.read
+            c = buffered_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)
+    val restricted_seq = new Restricted_Seq(seq, 0, stream_length)
 
     class Paged_Reader(override val offset: Int) extends Byte_Reader
     {
@@ -462,8 +463,19 @@
       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 }
+      def close { buffered_stream.close }
     }
     new Paged_Reader(0)
   }
+
+  def byte_reader(file: JFile): Byte_Reader =
+    make_byte_reader(new FileInputStream(file), file.length.toInt)
+
+  def byte_reader(url: URL): Byte_Reader =
+  {
+    val connection = url.openConnection
+    val stream = connection.getInputStream
+    val stream_length = connection.getContentLength
+    make_byte_reader(stream, stream_length)
+  }
 }