tuned signatures and messages;
authorwenzelm
Sun, 26 Sep 2010 19:32:45 +0200
changeset 39703 545cc67324d8
parent 39702 d7c256cb2797
child 39704 b4e0bddc9e4c
tuned signatures and messages;
src/Pure/System/cygwin.scala
src/Pure/System/download.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,
--- 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 {