lib/scripts/process
author nipkow
Tue, 18 Sep 2012 03:33:53 +0200
changeset 49433 1095f240146a
parent 39583 c1e9c6dfeff8
permissions -rwxr-xr-x
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
783f957dcb01 replaced setpgrp by more elaborate setsid;
wenzelm
parents: 26092
diff changeset
    15
if ($group eq "group") {
783f957dcb01 replaced setpgrp by more elaborate setsid;
wenzelm
parents: 26092
diff changeset
    16
  use POSIX "setsid";
26107
4b5e5fc1d11f removed junk;
wenzelm
parents: 26096
diff changeset
    17
  POSIX::setsid || die $!;
26096
783f957dcb01 replaced setpgrp by more elaborate setsid;
wenzelm
parents: 26092
diff changeset
    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