# HG changeset patch
# User wenzelm
# Date 1356958141 -3600
# Node ID 1fe68f1c3069beb6370d424b94597e82e3d651ec
# Parent  8922afc54b3d6570ca50408d587fc4f8bd2df4f1
tuned signature;

diff -r 8922afc54b3d -r 1fe68f1c3069 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Dec 31 13:34:47 2012 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Dec 31 13:49:01 2012 +0100
@@ -73,7 +73,7 @@
                 else Nil
               val cmdline =
                 shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
-              val (output, rc) = Standard_System.raw_exec(null, env, true, cmdline: _*)
+              val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
               if (rc != 0) error(output)
 
               val entries =
@@ -140,6 +140,40 @@
 
   /** external processes **/
 
+  /* raw execute for bootstrapping */
+
+  private def raw_execute(cwd: JFile, 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)
+    }
+    proc.redirectErrorStream(redirect)
+    proc.start
+  }
+
+  private def process_output(proc: Process): (String, Int) =
+  {
+    proc.getOutputStream.close
+    val output = File.read(proc.getInputStream)
+    val rc =
+      try { proc.waitFor }
+      finally {
+        proc.getInputStream.close
+        proc.getErrorStream.close
+        proc.destroy
+        Thread.interrupted
+      }
+    (output, rc)
+  }
+
+
   /* plain execute */
 
   def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
@@ -148,7 +182,7 @@
       if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
       else args
     val env1 = if (env == null) settings else settings ++ env
-    Standard_System.raw_execute(cwd, env1, redirect, cmdline: _*)
+    raw_execute(cwd, env1, redirect, cmdline: _*)
   }
 
   def execute(redirect: Boolean, args: String*): Process =
@@ -258,7 +292,7 @@
     } match {
       case Some(dir) =>
         val file = standard_path(dir + Path.basic(name))
-        Standard_System.process_output(execute(true, (List(file) ++ args): _*))
+        process_output(execute(true, (List(file) ++ args): _*))
       case None => ("Unknown Isabelle tool: " + name, 2)
     }
   }
diff -r 8922afc54b3d -r 1fe68f1c3069 src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Mon Dec 31 13:34:47 2012 +0100
+++ b/src/Pure/System/standard_system.scala	Mon Dec 31 13:49:01 2012 +0100
@@ -16,42 +16,6 @@
 
 object Standard_System
 {
-  /* shell processes */
-
-  def raw_execute(cwd: JFile, 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)
-    }
-    proc.redirectErrorStream(redirect)
-    proc.start
-  }
-
-  def process_output(proc: Process): (String, Int) =
-  {
-    proc.getOutputStream.close
-    val output = File.read(proc.getInputStream)
-    val rc =
-      try { proc.waitFor }
-      finally {
-        proc.getInputStream.close
-        proc.getErrorStream.close
-        proc.destroy
-        Thread.interrupted
-      }
-    (output, rc)
-  }
-
-  def raw_exec(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
-    : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
-
-
   /* cygwin_root */
 
   def cygwin_root(): String =