Standard_System.raw_exec;
authorwenzelm
Mon, 04 Jan 2010 22:43:07 +0100
changeset 34258 e936d3c35ce0
parent 34257 b5176fd9ab3c
child 34259 2ba492b8b6e8
Standard_System.raw_exec; more robust root.mkdirs;
src/Pure/System/cygwin.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/standard_system.scala
--- a/src/Pure/System/cygwin.scala	Mon Jan 04 22:35:32 2010 +0100
+++ b/src/Pure/System/cygwin.scala	Mon Jan 04 22:43:07 2010 +0100
@@ -104,7 +104,7 @@
 
   def setup(parent: Component, root: File)
   {
-    if (!root.mkdirs) error("Failed to create root directory: " + root)
+    if (!root.isDirectory && !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)
@@ -114,10 +114,9 @@
     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", "make,perl,python", "-q", "-n"))
+    val (_, rc) = Standard_System.raw_exec(root, null, true,
+        setup_exe.toString, "-R", root.toString, "-l", download.toString,
+    	    "-P", "make,perl,python", "-q", "-n")
     if (rc != 0) error("Cygwin setup failed!")
 
     sanity_check(root)
--- a/src/Pure/System/isabelle_system.scala	Mon Jan 04 22:35:32 2010 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Jan 04 22:43:07 2010 +0100
@@ -42,8 +42,7 @@
           if (Platform.is_windows) List(platform_root + "\\bin\\bash", "-l") else Nil
         val cmdline =
           shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
-        val (output, rc) =
-          Standard_System.process_output(Standard_System.raw_execute(null, env0, true, cmdline: _*))
+        val (output, rc) = Standard_System.raw_exec(null, env0, true, cmdline: _*)
         if (rc != 0) error(output)
 
         val entries =
--- a/src/Pure/System/standard_system.scala	Mon Jan 04 22:35:32 2010 +0100
+++ b/src/Pure/System/standard_system.scala	Mon Jan 04 22:43:07 2010 +0100
@@ -132,6 +132,9 @@
       }
     (output, rc)
   }
+
+  def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*):
+    (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
 }