# HG changeset patch
# User wenzelm
# Date 1285018586 -7200
# Node ID 48baf61cb888217cb19e31192cb40d193889ff9b
# Parent  c77b9374f45cbea4adcb17e8f52fc8da56576b63
refined ML/Scala bash wrapper, based on more general lib/scripts/process;

diff -r c77b9374f45c -r 48baf61cb888 lib/scripts/bash
--- a/lib/scripts/bash	Mon Sep 20 23:28:35 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Makarius
-#
-# bash - invoke shell command line (with robust signal handling)
-#
-
-use warnings;
-use strict;
-
-
-# args
-
-my ($group, $script_name, $pid_name, $output_name) = @ARGV;
-
-
-# process id
-
-if ($group eq "group") {
-  use POSIX "setsid";
-  POSIX::setsid || die $!;
-}
-
-open (PID_FILE, ">", $pid_name) || die $!;
-print PID_FILE "$$";
-close PID_FILE;
-
-
-# exec script
-
-exec qq/exec bash '$script_name' > '$output_name'/;
diff -r c77b9374f45c -r 48baf61cb888 lib/scripts/process
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/process	Mon Sep 20 23:36:26 2010 +0200
@@ -0,0 +1,34 @@
+#!/usr/bin/env perl
+#
+# Author: Makarius
+#
+# exec process - with optional process group and report of pid
+#
+
+use warnings;
+use strict;
+
+# args
+
+my ($group, $pid_name, $cmd_line) = @ARGV;
+
+
+# process group
+
+if ($group eq "group") {
+  use POSIX "setsid";
+  POSIX::setsid || die $!;
+}
+
+
+# pid
+
+open (PID_FILE, ">", $pid_name) || die $!;
+print PID_FILE "$$";
+close PID_FILE;
+
+
+# exec process
+
+exec "$cmd_line";
+
diff -r c77b9374f45c -r 48baf61cb888 src/Pure/ML-Systems/bash.ML
--- a/src/Pure/ML-Systems/bash.ML	Mon Sep 20 23:28:35 2010 +0200
+++ b/src/Pure/ML-Systems/bash.ML	Mon Sep 20 23:36:26 2010 +0200
@@ -25,8 +25,8 @@
     val output_name = OS.FileSys.tmpName ();
 
     val status =
-      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" nogroup " ^
-        script_name ^ " /dev/null " ^ output_name);
+      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" nogroup /dev/null" ^
+        " \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
     val rc =
       (case Posix.Process.fromStatus status of
         Posix.Process.W_EXITED => 0
diff -r c77b9374f45c -r 48baf61cb888 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 20 23:28:35 2010 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 20 23:36:26 2010 +0200
@@ -180,8 +180,8 @@
     val system_thread = Thread.fork (fn () =>
       let
         val status =
-          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" group " ^
-            script_name ^ " " ^ pid_name ^ " " ^ output_name);
+          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
+            " \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
         val res =
           (case Posix.Process.fromStatus status of
             Posix.Process.W_EXITED => Result 0
diff -r c77b9374f45c -r 48baf61cb888 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Sep 20 23:28:35 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Sep 20 23:36:26 2010 +0200
@@ -8,7 +8,8 @@
 
 import java.util.regex.Pattern
 import java.util.Locale
-import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File, IOException}
+import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File,
+  BufferedReader, InputStreamReader, IOException}
 import java.awt.{GraphicsEnvironment, Font}
 import java.awt.font.TextAttribute
 
@@ -200,58 +201,67 @@
   {
     Standard_System.with_tmp_file("isabelle_script") { script_file =>
       Standard_System.with_tmp_file("isabelle_pid") { pid_file =>
-        Standard_System.with_tmp_file("isabelle_output") { output_file =>
+
+        Standard_System.write_file(script_file, script)
 
-          Standard_System.write_file(script_file, script)
-
-          val proc = execute(true, expand_path("$ISABELLE_HOME/lib/scripts/bash"), "group",
-            script_file.getPath, pid_file.getPath, output_file.getPath)
+        val proc = execute(true, expand_path("$ISABELLE_HOME/lib/scripts/process"), "group",
+          posix_path(pid_file.getPath), "exec bash " + posix_path(script_file.getPath))
 
-          def kill(strict: Boolean) =
-          {
-            val pid =
-              try { Some(Standard_System.read_file(pid_file)) }
-              catch { case _: IOException => None }
-            if (pid.isDefined) {
-              var running = true
-              var count = 10   // FIXME property!?
-              while (running && count > 0) {
-                if (execute(true, "kill", "-INT", "-" + pid.get).waitFor != 0)
-                  running = false
-                else {
-                  Thread.sleep(100)   // FIXME property!?
-                  if (!strict) count -= 1
-                }
+        val stdout = new StringBuilder(100)
+        val stdout_thread = Simple_Thread.fork("stdout")
+        {
+          val reader =
+            new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
+          var c = -1
+          while ({ c = reader.read; c != -1 }) stdout += c.asInstanceOf[Char]
+          reader.close
+        }
+
+        def kill(strict: Boolean) =
+        {
+          val pid =
+            try { Some(Standard_System.read_file(pid_file)) }
+            catch { case _: IOException => None }
+          if (pid.isDefined) {
+            var running = true
+            var count = 10   // FIXME property!?
+            while (running && count > 0) {
+              if (execute(true, "kill", "-INT", "-" + pid.get).waitFor != 0)
+                running = false
+              else {
+                Thread.sleep(100)   // FIXME property!?
+                if (!strict) count -= 1
               }
             }
           }
+        }
 
-          val shutdown_hook = new Thread { override def run = kill(true) }
-          Runtime.getRuntime.addShutdownHook(shutdown_hook)  // FIXME tmp files during shutdown?!?
+        val shutdown_hook = new Thread { override def run = kill(true) }
+        Runtime.getRuntime.addShutdownHook(shutdown_hook)  // FIXME tmp files during shutdown?!?
 
-          def cleanup() =
-            try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
-            catch { case _: IllegalStateException => }
+        def cleanup() =
+          try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
+          catch { case _: IllegalStateException => }
 
-          val rc =
+        val rc =
+          try {
             try {
-              try { proc.waitFor }  // FIXME read stderr (!??)
-              catch { case e: InterruptedException => Thread.interrupted; kill(false); throw e }
+              val rc = proc.waitFor  // FIXME read stderr (!??)
+              stdout_thread.join
+              rc
             }
-            finally {
-              proc.getOutputStream.close
-              proc.getInputStream.close
-              proc.getErrorStream.close
-              proc.destroy
-              cleanup()
-            }
+            catch { case e: InterruptedException => Thread.interrupted; kill(false); throw e }
+          }
+          finally {
+            proc.getOutputStream.close
+            proc.getInputStream.close
+            proc.getErrorStream.close
+            proc.destroy
+            cleanup()
+          }
 
-          val output =
-            try { Standard_System.read_file(output_file) }
-            catch { case _: IOException => "" }
-
-          (output, rc)
-        }
+        stdout_thread.join()
+        (stdout.toString, rc)
       }
     }
   }