modernized perl scripts: prefer standalone executables;
authorwenzelm
Sun Feb 07 20:21:38 2010 +0100 (2010-02-07 ago)
changeset 3502316f9877abf0b
parent 35022 c844b93dd147
child 35024 0faeabd99289
modernized perl scripts: prefer standalone executables;
exec bash wrapper script directly -- avoid intermediate process;
lib/scripts/bash
lib/scripts/system.pl
src/Pure/ML-Systems/bash.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/System/isabelle_system.scala
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/scripts/bash	Sun Feb 07 20:21:38 2010 +0100
     1.3 @@ -0,0 +1,32 @@
     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 +$SIG{'INT'} = "DEFAULT";   #paranoia setting, required for Cygwin
    1.35 +exec qq/exec bash '$script_name' > '$output_name'/;
     2.1 --- a/lib/scripts/system.pl	Sun Feb 07 19:54:12 2010 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,28 +0,0 @@
     2.4 -#
     2.5 -# Author: Makarius
     2.6 -#
     2.7 -# system.pl - invoke shell command line (with robust signal handling)
     2.8 -#
     2.9 -
    2.10 -# args
    2.11 -
    2.12 -($group, $script_name, $pid_name, $output_name) = @ARGV;
    2.13 -
    2.14 -
    2.15 -# process id
    2.16 -
    2.17 -if ($group eq "group") {
    2.18 -  use POSIX "setsid";
    2.19 -  POSIX::setsid || die $!;
    2.20 -}
    2.21 -
    2.22 -open (PID_FILE, ">", $pid_name) || die $!;
    2.23 -print PID_FILE "$$";
    2.24 -close PID_FILE;
    2.25 -
    2.26 -
    2.27 -# exec script
    2.28 -
    2.29 -$SIG{'INT'} = "DEFAULT";   #paranoia setting, required for Cygwin
    2.30 -exec qq/exec bash '$script_name' > '$output_name'/;
    2.31 -
     3.1 --- a/src/Pure/ML-Systems/bash.ML	Sun Feb 07 19:54:12 2010 +0100
     3.2 +++ b/src/Pure/ML-Systems/bash.ML	Sun Feb 07 20:21:38 2010 +0100
     3.3 @@ -25,7 +25,7 @@
     3.4      val output_name = OS.FileSys.tmpName ();
     3.5  
     3.6      val status =
     3.7 -      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
     3.8 +      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" nogroup " ^
     3.9          script_name ^ " /dev/null " ^ output_name);
    3.10      val rc =
    3.11        (case Posix.Process.fromStatus status of
     4.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Feb 07 19:54:12 2010 +0100
     4.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Feb 07 20:21:38 2010 +0100
     4.3 @@ -180,7 +180,7 @@
     4.4      val system_thread = Thread.fork (fn () =>
     4.5        let
     4.6          val status =
     4.7 -          OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" group " ^
     4.8 +          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" group " ^
     4.9              script_name ^ " " ^ pid_name ^ " " ^ output_name);
    4.10          val res =
    4.11            (case Posix.Process.fromStatus status of
     5.1 --- a/src/Pure/System/isabelle_system.scala	Sun Feb 07 19:54:12 2010 +0100
     5.2 +++ b/src/Pure/System/isabelle_system.scala	Sun Feb 07 20:21:38 2010 +0100
     5.3 @@ -170,8 +170,7 @@
     5.4  
     5.5            Standard_System.write_file(script_file, script)
     5.6  
     5.7 -          val proc = execute(true, "perl", "-w",
     5.8 -            expand_path("$ISABELLE_HOME/lib/scripts/system.pl"), "group",
     5.9 +          val proc = execute(true, expand_path("$ISABELLE_HOME/lib/scripts/bash"), "group",
    5.10              script_file.getPath, pid_file.getPath, output_file.getPath)
    5.11  
    5.12            def kill(strict: Boolean) =