# HG changeset patch # User wenzelm # Date 1285522365 -7200 # Node ID 545cc67324d8b79268c0f312f35eccef94072bef # Parent d7c256cb2797766991106f50f512393646240bc7 tuned signatures and messages; diff -r d7c256cb2797 -r 545cc67324d8 src/Pure/System/cygwin.scala --- a/src/Pure/System/cygwin.scala Sat Sep 25 17:28:41 2010 +0200 +++ b/src/Pure/System/cygwin.scala Sun Sep 26 19:32:45 2010 +0200 @@ -111,7 +111,9 @@ val setup_exe = new File(root, "setup.exe") - try { Download.file(parent, new URL("http://www.cygwin.com/setup.exe"), setup_exe) } + try { + Download.file(parent, "Downloading", new URL("http://www.cygwin.com/setup.exe"), setup_exe) + } catch { case _: RuntimeException => error("Failed to download Cygwin setup program") } val (_, rc) = Standard_System.raw_exec(root, null, true, diff -r d7c256cb2797 -r 545cc67324d8 src/Pure/System/download.scala --- a/src/Pure/System/download.scala Sat Sep 25 17:28:41 2010 +0200 +++ b/src/Pure/System/download.scala Sun Sep 26 19:32:45 2010 +0200 @@ -16,11 +16,11 @@ object Download { - def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) = + def stream(parent: Component, title: String, url: URL): (URLConnection, BufferedInputStream) = { val connection = url.openConnection - val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream) + val stream = new ProgressMonitorInputStream(parent, title, connection.getInputStream) val monitor = stream.getProgressMonitor monitor.setNote(connection.getURL.toString) @@ -30,14 +30,14 @@ (connection, new BufferedInputStream(stream)) } - def file(parent: Component, url: URL, file: File) + def file(parent: Component, title: String, url: URL, file: File) { - val (connection, instream) = stream(parent, url) + val (connection, instream) = stream(parent, title, url) val mod_time = connection.getLastModified def read() = try { instream.read } - catch { case _ : InterruptedIOException => error("Download canceled!") } + catch { case _ : InterruptedIOException => error("Canceled by user") } try { val outstream = new BufferedOutputStream(new FileOutputStream(file)) try {