--- a/src/Pure/Admin/component_cygwin.scala Sun Mar 26 19:31:05 2023 +0200
+++ b/src/Pure/Admin/component_cygwin.scala Sun Mar 26 19:36:00 2023 +0200
@@ -29,7 +29,7 @@
val cygwin_exe_name = mirror + "/setup-x86_64.exe"
val cygwin_exe = cygwin_isabelle + Path.explode("cygwin.exe")
Bytes.write(cygwin_exe,
- try { Bytes.read(Url(cygwin_exe_name)) }
+ try { Bytes.read_url(cygwin_exe_name) }
catch { case ERROR(_) => error("Failed to download " + quote(cygwin_exe_name)) })
File.write(cygwin_isabelle + Path.explode("cygwin_mirror"), mirror)
--- a/src/Pure/General/bytes.scala Sun Mar 26 19:31:05 2023 +0200
+++ b/src/Pure/General/bytes.scala Sun Mar 26 19:36:00 2023 +0200
@@ -69,6 +69,8 @@
new Bytes(out.toByteArray, 0, out.size)
}
+ def read_url(name: String): Bytes = using(Url(name).openStream)(read_stream(_))
+
def read(file: JFile): Bytes = {
val length = file.length
val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt
@@ -77,8 +79,6 @@
def read(path: Path): Bytes = read(path.file)
- def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
-
def read_slice(path: Path, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = {
val start = offset.max(0L)
val len = (path.file.length - start).max(0L).min(limit)