| author | wenzelm | 
| Thu, 09 Jul 2015 00:40:57 +0200 | |
| changeset 60698 | 29e8bdc41f90 | 
| parent 39583 | c1e9c6dfeff8 | 
| permissions | -rwxr-xr-x | 
| 35023 
16f9877abf0b
modernized perl scripts: prefer standalone executables;
 wenzelm parents: 
34197diff
changeset | 1 | #!/usr/bin/env perl | 
| 26092 
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
 wenzelm parents: diff
changeset | 2 | # | 
| 
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
 wenzelm parents: diff
changeset | 3 | # Author: Makarius | 
| 
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
 wenzelm parents: diff
changeset | 4 | # | 
| 39576 
48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
 wenzelm parents: 
35024diff
changeset | 5 | # exec process - with optional process group and report of pid | 
| 26092 
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
 wenzelm parents: diff
changeset | 6 | # | 
| 
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
 wenzelm parents: diff
changeset | 7 | |
| 35023 
16f9877abf0b
modernized perl scripts: prefer standalone executables;
 wenzelm parents: 
34197diff
changeset | 8 | use warnings; | 
| 
16f9877abf0b
modernized perl scripts: prefer standalone executables;
 wenzelm parents: 
34197diff
changeset | 9 | use strict; | 
| 
16f9877abf0b
modernized perl scripts: prefer standalone executables;
 wenzelm parents: 
34197diff
changeset | 10 | |
| 39583 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 11 | # process group | 
| 26092 
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
 wenzelm parents: diff
changeset | 12 | |
| 39583 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 13 | my $group = $ARGV[0]; shift(@ARGV); | 
| 26092 
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
 wenzelm parents: diff
changeset | 14 | |
| 26096 | 15 | if ($group eq "group") {
 | 
| 16 | use POSIX "setsid"; | |
| 26107 | 17 | POSIX::setsid || die $!; | 
| 26096 | 18 | } | 
| 26092 
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
 wenzelm parents: diff
changeset | 19 | |
| 39576 
48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
 wenzelm parents: 
35024diff
changeset | 20 | |
| 39583 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 21 | # report pid | 
| 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 22 | |
| 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 23 | my $pid_name = $ARGV[0]; shift(@ARGV); | 
| 39576 
48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
 wenzelm parents: 
35024diff
changeset | 24 | |
| 39581 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 wenzelm parents: 
39576diff
changeset | 25 | if ($pid_name eq "-") {
 | 
| 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 wenzelm parents: 
39576diff
changeset | 26 | print "$$\n"; | 
| 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 wenzelm parents: 
39576diff
changeset | 27 | } | 
| 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 wenzelm parents: 
39576diff
changeset | 28 | else {
 | 
| 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 wenzelm parents: 
39576diff
changeset | 29 | open (PID_FILE, ">", $pid_name) || die $!; | 
| 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 wenzelm parents: 
39576diff
changeset | 30 | print PID_FILE "$$"; | 
| 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 wenzelm parents: 
39576diff
changeset | 31 | close PID_FILE; | 
| 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 wenzelm parents: 
39576diff
changeset | 32 | } | 
| 26092 
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
 wenzelm parents: diff
changeset | 33 | |
| 
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
 wenzelm parents: diff
changeset | 34 | |
| 39576 
48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
 wenzelm parents: 
35024diff
changeset | 35 | # exec process | 
| 26092 
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
 wenzelm parents: diff
changeset | 36 | |
| 39583 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 37 | my $script = $ARGV[0]; shift(@ARGV); | 
| 39576 
48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
 wenzelm parents: 
35024diff
changeset | 38 | |
| 39583 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 39 | if ($script eq "script") {
 | 
| 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 40 | my $cmd_line = $ARGV[0]; shift(@ARGV); | 
| 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 41 | exec $cmd_line || die $!; | 
| 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 42 | } | 
| 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 43 | else {
 | 
| 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 44 |   (exec { $ARGV[0] } @ARGV) || die $!;
 | 
| 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 45 | } | 
| 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 wenzelm parents: 
39581diff
changeset | 46 |