# 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) } }