# HG changeset patch
# User wenzelm
# Date 1262459284 -3600
# Node ID f7a0088518e18fca7cba5f405c78e1d4e846389f
# Parent  d37cfca6988736de41ec89200b798822d37dd7f8
tuned error handling;

diff -r d37cfca69887 -r f7a0088518e1 src/Pure/General/download.scala
--- a/src/Pure/General/download.scala	Sat Jan 02 01:14:49 2010 +0100
+++ b/src/Pure/General/download.scala	Sat Jan 02 20:08:04 2010 +0100
@@ -7,7 +7,8 @@
 package isabelle
 
 
-import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream, File}
+import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream,
+  File, InterruptedIOException}
 import java.net.{URL, URLConnection}
 import java.awt.{Component, HeadlessException}
 import javax.swing.ProgressMonitorInputStream
@@ -29,20 +30,24 @@
     (connection, new BufferedInputStream(stream))
   }
 
-  // FIXME error handling (dialogs)
-  def file(parent: Component, url: URL, file: File): Boolean =
+  def file(parent: Component, url: URL, file: File)
   {
-    val outstream = new BufferedOutputStream(new FileOutputStream(file))
-
     val (connection, instream) = stream(parent, url)
     val mod_time = connection.getLastModified
 
-    var c: Int = 0
-    while ({ c = instream.read; c != -1}) outstream.write(c)
-
-    instream.close
-    outstream.close
-    file.setLastModified(mod_time)
+    def read() =
+      try { instream.read }
+      catch { case _ : InterruptedIOException => error("Download canceled!") }
+    try {
+      val outstream = new BufferedOutputStream(new FileOutputStream(file))
+      try {
+        var c: Int = 0
+        while ({ c = read(); c != -1}) outstream.write(c)
+      }
+      finally { outstream.close }
+      if (mod_time > 0) file.setLastModified(mod_time)
+    }
+    finally { instream.close }
   }
 }
 
diff -r d37cfca69887 -r f7a0088518e1 src/Pure/System/cygwin.scala
--- a/src/Pure/System/cygwin.scala	Sat Jan 02 01:14:49 2010 +0100
+++ b/src/Pure/System/cygwin.scala	Sat Jan 02 20:08:04 2010 +0100
@@ -81,6 +81,14 @@
   private val CYGWIN_SETUP1 = "Software\\Cygwin\\setup"
   private val CYGWIN_SETUP2 = "Software\\Wow6432Node\\Cygwin\\setup"
 
+  private def sanity_check(root: File)
+  {
+    if (!new File(root, "bin\\bash.exe").isFile ||
+        !new File(root, "bin\\env.exe").isFile ||
+        !new File(root, "bin\\tar.exe").isFile)
+      error("Bad Cygwin installation: " + root.toString)
+  }
+
   def check_root(): String =
   {
     val root_env = java.lang.System.getenv("CYGWIN_ROOT")
@@ -90,14 +98,10 @@
         query_registry(CYGWIN_SETUP1, "rootdir") orElse
         query_registry(CYGWIN_SETUP2, "rootdir") getOrElse
         error("Failed to determine Cygwin installation -- version 1.7 required")
-    val ok =
-      new File(root + "\\bin\\bash.exe").isFile &&
-      new File(root + "\\bin\\env.exe").isFile
-    if (!ok) error("Bad Cygwin installation: " + root)
+    sanity_check(new File(root))
     root
   }
 
-  // FIXME error handling (dialogs)
   def setup(parent: Component, root: File)
   {
     if (!root.mkdirs) error("Failed to create root directory: " + root)
@@ -106,14 +110,17 @@
     if (!download.mkdir) error("Failed to create download directory: " + download)
 
     val setup_exe = new File(root, "setup.exe")
-    if (!Download.file(parent, new URL("http://www.cygwin.com/setup.exe"), setup_exe))
-      error("Failed to download Cygwin setup program")
+
+    try { Download.file(parent, new URL("http://www.cygwin.com/setup.exe"), setup_exe) }
+    catch { case _: RuntimeException => error("Failed to download Cygwin setup program") }
 
     val (_, rc) = Standard_System.process_output(
     	Standard_System.raw_execute(root, null, true,
     	  setup_exe.toString, "-R", root.toString, "-l", download.toString,
     	    "-P", "perl,python", "-q", "-n"))
     if (rc != 0) error("Cygwin setup failed!")
+
+    sanity_check(root)
   }
 }