refined ML/Scala bash wrapper, based on more general lib/scripts/process;
authorwenzelm
Mon Sep 20 23:36:26 2010 +0200 (2010-09-20 ago)
changeset 3957648baf61cb888
parent 39575 c77b9374f45c
child 39577 51bcd6003984
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
lib/scripts/bash
lib/scripts/process
src/Pure/ML-Systems/bash.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/System/isabelle_system.scala
     1.1 --- a/lib/scripts/bash	Mon Sep 20 23:28:35 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,31 +0,0 @@
     1.4 -#!/usr/bin/env perl
     1.5 -#
     1.6 -# Author: Makarius
     1.7 -#
     1.8 -# bash - invoke shell command line (with robust signal handling)
     1.9 -#
    1.10 -
    1.11 -use warnings;
    1.12 -use strict;
    1.13 -
    1.14 -
    1.15 -# args
    1.16 -
    1.17 -my ($group, $script_name, $pid_name, $output_name) = @ARGV;
    1.18 -
    1.19 -
    1.20 -# process id
    1.21 -
    1.22 -if ($group eq "group") {
    1.23 -  use POSIX "setsid";
    1.24 -  POSIX::setsid || die $!;
    1.25 -}
    1.26 -
    1.27 -open (PID_FILE, ">", $pid_name) || die $!;
    1.28 -print PID_FILE "$$";
    1.29 -close PID_FILE;
    1.30 -
    1.31 -
    1.32 -# exec script
    1.33 -
    1.34 -exec qq/exec bash '$script_name' > '$output_name'/;
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/scripts/process	Mon Sep 20 23:36:26 2010 +0200
     2.3 @@ -0,0 +1,34 @@
     2.4 +#!/usr/bin/env perl
     2.5 +#
     2.6 +# Author: Makarius
     2.7 +#
     2.8 +# exec process - with optional process group and report of pid
     2.9 +#
    2.10 +
    2.11 +use warnings;
    2.12 +use strict;
    2.13 +
    2.14 +# args
    2.15 +
    2.16 +my ($group, $pid_name, $cmd_line) = @ARGV;
    2.17 +
    2.18 +
    2.19 +# process group
    2.20 +
    2.21 +if ($group eq "group") {
    2.22 +  use POSIX "setsid";
    2.23 +  POSIX::setsid || die $!;
    2.24 +}
    2.25 +
    2.26 +
    2.27 +# pid
    2.28 +
    2.29 +open (PID_FILE, ">", $pid_name) || die $!;
    2.30 +print PID_FILE "$$";
    2.31 +close PID_FILE;
    2.32 +
    2.33 +
    2.34 +# exec process
    2.35 +
    2.36 +exec "$cmd_line";
    2.37 +
     3.1 --- a/src/Pure/ML-Systems/bash.ML	Mon Sep 20 23:28:35 2010 +0200
     3.2 +++ b/src/Pure/ML-Systems/bash.ML	Mon Sep 20 23:36:26 2010 +0200
     3.3 @@ -25,8 +25,8 @@
     3.4      val output_name = OS.FileSys.tmpName ();
     3.5  
     3.6      val status =
     3.7 -      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" nogroup " ^
     3.8 -        script_name ^ " /dev/null " ^ output_name);
     3.9 +      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" nogroup /dev/null" ^
    3.10 +        " \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
    3.11      val rc =
    3.12        (case Posix.Process.fromStatus status of
    3.13          Posix.Process.W_EXITED => 0
     4.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 20 23:28:35 2010 +0200
     4.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 20 23:36:26 2010 +0200
     4.3 @@ -180,8 +180,8 @@
     4.4      val system_thread = Thread.fork (fn () =>
     4.5        let
     4.6          val status =
     4.7 -          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" group " ^
     4.8 -            script_name ^ " " ^ pid_name ^ " " ^ output_name);
     4.9 +          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
    4.10 +            " \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
    4.11          val res =
    4.12            (case Posix.Process.fromStatus status of
    4.13              Posix.Process.W_EXITED => Result 0
     5.1 --- a/src/Pure/System/isabelle_system.scala	Mon Sep 20 23:28:35 2010 +0200
     5.2 +++ b/src/Pure/System/isabelle_system.scala	Mon Sep 20 23:36:26 2010 +0200
     5.3 @@ -8,7 +8,8 @@
     5.4  
     5.5  import java.util.regex.Pattern
     5.6  import java.util.Locale
     5.7 -import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File, IOException}
     5.8 +import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File,
     5.9 +  BufferedReader, InputStreamReader, IOException}
    5.10  import java.awt.{GraphicsEnvironment, Font}
    5.11  import java.awt.font.TextAttribute
    5.12  
    5.13 @@ -200,58 +201,67 @@
    5.14    {
    5.15      Standard_System.with_tmp_file("isabelle_script") { script_file =>
    5.16        Standard_System.with_tmp_file("isabelle_pid") { pid_file =>
    5.17 -        Standard_System.with_tmp_file("isabelle_output") { output_file =>
    5.18 +
    5.19 +        Standard_System.write_file(script_file, script)
    5.20  
    5.21 -          Standard_System.write_file(script_file, script)
    5.22 -
    5.23 -          val proc = execute(true, expand_path("$ISABELLE_HOME/lib/scripts/bash"), "group",
    5.24 -            script_file.getPath, pid_file.getPath, output_file.getPath)
    5.25 +        val proc = execute(true, expand_path("$ISABELLE_HOME/lib/scripts/process"), "group",
    5.26 +          posix_path(pid_file.getPath), "exec bash " + posix_path(script_file.getPath))
    5.27  
    5.28 -          def kill(strict: Boolean) =
    5.29 -          {
    5.30 -            val pid =
    5.31 -              try { Some(Standard_System.read_file(pid_file)) }
    5.32 -              catch { case _: IOException => None }
    5.33 -            if (pid.isDefined) {
    5.34 -              var running = true
    5.35 -              var count = 10   // FIXME property!?
    5.36 -              while (running && count > 0) {
    5.37 -                if (execute(true, "kill", "-INT", "-" + pid.get).waitFor != 0)
    5.38 -                  running = false
    5.39 -                else {
    5.40 -                  Thread.sleep(100)   // FIXME property!?
    5.41 -                  if (!strict) count -= 1
    5.42 -                }
    5.43 +        val stdout = new StringBuilder(100)
    5.44 +        val stdout_thread = Simple_Thread.fork("stdout")
    5.45 +        {
    5.46 +          val reader =
    5.47 +            new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
    5.48 +          var c = -1
    5.49 +          while ({ c = reader.read; c != -1 }) stdout += c.asInstanceOf[Char]
    5.50 +          reader.close
    5.51 +        }
    5.52 +
    5.53 +        def kill(strict: Boolean) =
    5.54 +        {
    5.55 +          val pid =
    5.56 +            try { Some(Standard_System.read_file(pid_file)) }
    5.57 +            catch { case _: IOException => None }
    5.58 +          if (pid.isDefined) {
    5.59 +            var running = true
    5.60 +            var count = 10   // FIXME property!?
    5.61 +            while (running && count > 0) {
    5.62 +              if (execute(true, "kill", "-INT", "-" + pid.get).waitFor != 0)
    5.63 +                running = false
    5.64 +              else {
    5.65 +                Thread.sleep(100)   // FIXME property!?
    5.66 +                if (!strict) count -= 1
    5.67                }
    5.68              }
    5.69            }
    5.70 +        }
    5.71  
    5.72 -          val shutdown_hook = new Thread { override def run = kill(true) }
    5.73 -          Runtime.getRuntime.addShutdownHook(shutdown_hook)  // FIXME tmp files during shutdown?!?
    5.74 +        val shutdown_hook = new Thread { override def run = kill(true) }
    5.75 +        Runtime.getRuntime.addShutdownHook(shutdown_hook)  // FIXME tmp files during shutdown?!?
    5.76  
    5.77 -          def cleanup() =
    5.78 -            try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
    5.79 -            catch { case _: IllegalStateException => }
    5.80 +        def cleanup() =
    5.81 +          try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
    5.82 +          catch { case _: IllegalStateException => }
    5.83  
    5.84 -          val rc =
    5.85 +        val rc =
    5.86 +          try {
    5.87              try {
    5.88 -              try { proc.waitFor }  // FIXME read stderr (!??)
    5.89 -              catch { case e: InterruptedException => Thread.interrupted; kill(false); throw e }
    5.90 +              val rc = proc.waitFor  // FIXME read stderr (!??)
    5.91 +              stdout_thread.join
    5.92 +              rc
    5.93              }
    5.94 -            finally {
    5.95 -              proc.getOutputStream.close
    5.96 -              proc.getInputStream.close
    5.97 -              proc.getErrorStream.close
    5.98 -              proc.destroy
    5.99 -              cleanup()
   5.100 -            }
   5.101 +            catch { case e: InterruptedException => Thread.interrupted; kill(false); throw e }
   5.102 +          }
   5.103 +          finally {
   5.104 +            proc.getOutputStream.close
   5.105 +            proc.getInputStream.close
   5.106 +            proc.getErrorStream.close
   5.107 +            proc.destroy
   5.108 +            cleanup()
   5.109 +          }
   5.110  
   5.111 -          val output =
   5.112 -            try { Standard_System.read_file(output_file) }
   5.113 -            catch { case _: IOException => "" }
   5.114 -
   5.115 -          (output, rc)
   5.116 -        }
   5.117 +        stdout_thread.join()
   5.118 +        (stdout.toString, rc)
   5.119        }
   5.120      }
   5.121    }