# HG changeset patch
# User wenzelm
# Date 1230392066 -3600
# Node ID f27d63717075b5b8dfe528c5191945b4eb3c3b15
# Parent  f1ce1e2229c6a76f3ae7643e5511e93cc63a789c# Parent  d41ccf3efbfc91c9e05c3989080490b01b3fd42e
merged

diff -r f1ce1e2229c6 -r f27d63717075 src/Pure/Tools/isabelle_process.scala
--- a/src/Pure/Tools/isabelle_process.scala	Sat Dec 27 16:28:36 2008 +0100
+++ b/src/Pure/Tools/isabelle_process.scala	Sat Dec 27 16:34:26 2008 +0100
@@ -125,7 +125,7 @@
     if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
     else {
       try {
-        if (isabelle_system.exec("kill", "-INT", pid).waitFor == 0)
+        if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0)
           put_result(Kind.SIGNAL, null, "INT")
         else
           put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
@@ -360,7 +360,7 @@
     try {
       val cmdline =
         List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
-      proc = isabelle_system.exec2(cmdline: _*)
+      proc = isabelle_system.execute(true, cmdline: _*)
     }
     catch {
       case e: IOException =>
diff -r f1ce1e2229c6 -r f27d63717075 src/Pure/Tools/isabelle_system.scala
--- a/src/Pure/Tools/isabelle_system.scala	Sat Dec 27 16:28:36 2008 +0100
+++ b/src/Pure/Tools/isabelle_system.scala	Sat Dec 27 16:34:26 2008 +0100
@@ -19,17 +19,19 @@
 
   /* Isabelle environment settings */
 
+  private val environment = System.getenv
+
   def getenv(name: String) = {
-    val value = System.getenv(if (name == "HOME") "HOME_JVM" else name)
+    val value = environment.get(if (name == "HOME") "HOME_JVM" else name)
     if (value != null) value else ""
   }
 
   def getenv_strict(name: String) = {
-    val value = getenv(name)
+    val value = environment.get(name)
     if (value != "") value else error("Undefined environment variable: " + name)
   }
 
-  def is_cygwin() = Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM"))
+  val is_cygwin = Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM"))
 
 
   /* file path specifications */
@@ -80,14 +82,14 @@
 
   /* processes */
 
-  private def posix_prefix() = if (is_cygwin()) List(platform_path("/bin/env")) else Nil
-
-  def exec(args: String*): Process = Runtime.getRuntime.exec((posix_prefix() ++ args).toArray)
+  def execute(redirect: Boolean, args: String*): Process = {
+    val cmdline = new java.util.LinkedList[String]
+    if (is_cygwin) cmdline.add(platform_path("/bin/env"))
+    for (s <- args) cmdline.add(s)
 
-  def exec2(args: String*): Process = {
-    val cmdline = new java.util.LinkedList[String]
-    for (s <- posix_prefix() ++ args) cmdline.add(s)
-    new ProcessBuilder(cmdline).redirectErrorStream(true).start
+    val proc = new ProcessBuilder(cmdline)
+    val env = proc.environment; env.clear; env.putAll(environment)
+    proc.redirectErrorStream(redirect).start
   }
 
 
@@ -95,7 +97,7 @@
 
   def isabelle_tool(args: String*) = {
     val proc =
-      try { exec2((List(getenv_strict("ISABELLE_TOOL")) ++ args): _*) }
+      try { execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*) }
       catch { case e: IOException => error(e.getMessage) }
     proc.getOutputStream.close
     val output = Source.fromInputStream(proc.getInputStream, charset).mkString
@@ -117,10 +119,13 @@
     if (rc != 0) error(result)
   }
 
-  def fifo_reader(fifo: String) =  // blocks until writer is ready
-    if (is_cygwin()) new BufferedReader(new InputStreamReader(Runtime.getRuntime.exec(
-      Array(platform_path("/bin/cat"), fifo)).getInputStream, charset))
-    else new BufferedReader(new InputStreamReader(new FileInputStream(fifo), charset))
+  def fifo_reader(fifo: String) = {
+    // blocks until writer is ready
+    val stream =
+      if (is_cygwin) execute(false, "cat", fifo).getInputStream
+      else new FileInputStream(fifo)
+    new BufferedReader(new InputStreamReader(stream, charset))
+  }
 
 
   /* find logics */