Standard_System.raw_execute: optional cwd;
basic Cygwin.setup with download and unattended installation;

--- a/src/Pure/General/download.scala	Sat Jan 02 00:08:47 2010 +0100
+++ b/src/Pure/General/download.scala	Sat Jan 02 01:14:49 2010 +0100
@@ -29,8 +29,8 @@
     (connection, new BufferedInputStream(stream))
   }
 
-  // FIXME error handling
-  def file(parent: Component, url: URL, file: File)
+  // FIXME error handling (dialogs)
+  def file(parent: Component, url: URL, file: File): Boolean =
   {
     val outstream = new BufferedOutputStream(new FileOutputStream(file))
 

--- a/src/Pure/System/cygwin.scala	Sat Jan 02 00:08:47 2010 +0100
+++ b/src/Pure/System/cygwin.scala	Sat Jan 02 01:14:49 2010 +0100
@@ -8,6 +8,8 @@
 
 import java.lang.reflect.Method
 import java.io.File
+import java.net.URL
+import java.awt.Component
 
 
 object Cygwin
@@ -95,13 +97,23 @@
     root
   }
 
-  def setup(exe: String, root: String): Int =
+  // FIXME error handling (dialogs)
+  def setup(parent: Component, root: File)
   {
-    val (output, rc) = Standard_System.process_output(
-    	Standard_System.raw_execute(null, true, exe, "-R", root, "-P", "perl,python", "-q", "-n"))
-    val root_dir = new File(root)
-    if (root_dir.isDirectory) Standard_System.write_file(new File(root, "setup.log"), output)
-    rc
+    if (!root.mkdirs) error("Failed to create root directory: " + root)
+
+    val download = new File(root, "download")
+    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")
+
+    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!")
   }
 }
 

--- a/src/Pure/System/isabelle_system.scala	Sat Jan 02 00:08:47 2010 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sat Jan 02 01:14:49 2010 +0100
@@ -43,7 +43,7 @@
         val cmdline =
           shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
         val (output, rc) =
-          Standard_System.process_output(Standard_System.raw_execute(env0, true, cmdline: _*))
+          Standard_System.process_output(Standard_System.raw_execute(null, env0, true, cmdline: _*))
         if (rc != 0) error(output)
 
         val entries =
@@ -66,7 +66,7 @@
     val cmdline =
       if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
       else args
-    Standard_System.raw_execute(environment, redirect, cmdline: _*)
+    Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
   }
 
 

--- a/src/Pure/System/standard_system.scala	Sat Jan 02 00:08:47 2010 +0100
+++ b/src/Pure/System/standard_system.scala	Sat Jan 02 01:14:49 2010 +0100
@@ -101,12 +101,13 @@
 
   /* shell processes */
 
-  def raw_execute(env: Map[String, String], redirect: Boolean, args: String*): Process =
+  def raw_execute(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
   {
     val cmdline = new java.util.LinkedList[String]
     for (s <- args) cmdline.add(s)
 
     val proc = new ProcessBuilder(cmdline)
+    if (cwd != null) proc.directory(cwd)
     if (env != null) {
       proc.environment.clear
       for ((x, y) <- env) proc.environment.put(x, y)