# HG changeset patch
# User wenzelm
# Date 1219944599 -7200
# Node ID 1447932b1b135c9b744824cff612a946b512e7af
# Parent  1a6f273108aed314735e7150867d12b2298c48fc
added is_cygwin;
added exec2, which joins stdout/stderr;
tuned thread arrangement;

diff -r 1a6f273108ae -r 1447932b1b13 src/Pure/Tools/isabelle_system.scala
--- a/src/Pure/Tools/isabelle_system.scala	Thu Aug 28 19:29:58 2008 +0200
+++ b/src/Pure/Tools/isabelle_system.scala	Thu Aug 28 19:29:59 2008 +0200
@@ -13,7 +13,7 @@
 
 object IsabelleSystem {
 
-  /* Isabelle settings */
+  /* Isabelle environment settings */
 
   def getenv(name: String) = {
     val value = System.getenv(name)
@@ -25,6 +25,8 @@
     if (value != "") value else error("Undefined environment variable: " + name)
   }
 
+  def is_cygwin() = Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM"))
+
 
   /* file path specifications */
 
@@ -71,12 +73,14 @@
 
   /* processes */
 
-  private def posix_prefix() = {
-    if (Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM")))
-      List(platform_path("/bin/env"))
-    else Nil
-  }
+  private def posix_prefix() = if (is_cygwin()) List(platform_path("/bin/env")) else Nil
 
   def exec(args: List[String]) = Runtime.getRuntime.exec((posix_prefix() ++ args).toArray)
 
+  def exec2(args: List[String]) = {
+    val cmdline = new java.util.LinkedList[String]
+    for (s <- posix_prefix() ++ args) cmdline.add(s)
+    new ProcessBuilder(cmdline).redirectErrorStream(true).start
+  }
+
 }