| author | blanchet | 
| Mon, 29 Sep 2014 18:37:33 +0200 | |
| changeset 58482 | 7836013951e6 | 
| parent 39583 | c1e9c6dfeff8 | 
| permissions | -rwxr-xr-x | 
| 
35023
 
16f9877abf0b
modernized perl scripts: prefer standalone executables;
 
wenzelm 
parents: 
34197 
diff
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: 
35024 
diff
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: 
34197 
diff
changeset
 | 
8  | 
use warnings;  | 
| 
 
16f9877abf0b
modernized perl scripts: prefer standalone executables;
 
wenzelm 
parents: 
34197 
diff
changeset
 | 
9  | 
use strict;  | 
| 
 
16f9877abf0b
modernized perl scripts: prefer standalone executables;
 
wenzelm 
parents: 
34197 
diff
changeset
 | 
10  | 
|
| 
39583
 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 
wenzelm 
parents: 
39581 
diff
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: 
39581 
diff
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: 
35024 
diff
changeset
 | 
20  | 
|
| 
39583
 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 
wenzelm 
parents: 
39581 
diff
changeset
 | 
21  | 
# report pid  | 
| 
 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 
wenzelm 
parents: 
39581 
diff
changeset
 | 
22  | 
|
| 
 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 
wenzelm 
parents: 
39581 
diff
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: 
35024 
diff
changeset
 | 
24  | 
|
| 
39581
 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 
wenzelm 
parents: 
39576 
diff
changeset
 | 
25  | 
if ($pid_name eq "-") {
 | 
| 
 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 
wenzelm 
parents: 
39576 
diff
changeset
 | 
26  | 
print "$$\n";  | 
| 
 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 
wenzelm 
parents: 
39576 
diff
changeset
 | 
27  | 
}  | 
| 
 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 
wenzelm 
parents: 
39576 
diff
changeset
 | 
28  | 
else {
 | 
| 
 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 
wenzelm 
parents: 
39576 
diff
changeset
 | 
29  | 
open (PID_FILE, ">", $pid_name) || die $!;  | 
| 
 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 
wenzelm 
parents: 
39576 
diff
changeset
 | 
30  | 
print PID_FILE "$$";  | 
| 
 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 
wenzelm 
parents: 
39576 
diff
changeset
 | 
31  | 
close PID_FILE;  | 
| 
 
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
 
wenzelm 
parents: 
39576 
diff
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: 
35024 
diff
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: 
39581 
diff
changeset
 | 
37  | 
my $script = $ARGV[0]; shift(@ARGV);  | 
| 
39576
 
48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
 
wenzelm 
parents: 
35024 
diff
changeset
 | 
38  | 
|
| 
39583
 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 
wenzelm 
parents: 
39581 
diff
changeset
 | 
39  | 
if ($script eq "script") {
 | 
| 
 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 
wenzelm 
parents: 
39581 
diff
changeset
 | 
40  | 
my $cmd_line = $ARGV[0]; shift(@ARGV);  | 
| 
 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 
wenzelm 
parents: 
39581 
diff
changeset
 | 
41  | 
exec $cmd_line || die $!;  | 
| 
 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 
wenzelm 
parents: 
39581 
diff
changeset
 | 
42  | 
}  | 
| 
 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 
wenzelm 
parents: 
39581 
diff
changeset
 | 
43  | 
else {
 | 
| 
 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 
wenzelm 
parents: 
39581 
diff
changeset
 | 
44  | 
  (exec { $ARGV[0] } @ARGV) || die $!;
 | 
| 
 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 
wenzelm 
parents: 
39581 
diff
changeset
 | 
45  | 
}  | 
| 
 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
 
wenzelm 
parents: 
39581 
diff
changeset
 | 
46  |