--- 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'/;
--- /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";
+
--- 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
--- 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
--- 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)
}
}
}