lib/scripts/feeder
author wenzelm
Tue, 08 Apr 2008 15:47:10 +0200
changeset 26576 fc76b7b79ba9
parent 15847 c05c7670f166
child 29145 b1c6f4563df7
permissions -rwxr-xr-x
removed obsolete AUTO_PERL feature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10512
diff changeset
     1
#!/usr/bin/env bash
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     2
#
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     3
# $Id$
9789
wenzelm
parents: 6082
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     5
#
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     6
# feeder - feed isabelle session
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     7
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     8
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     9
## diagnostics
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    10
10512
wenzelm
parents: 9789
diff changeset
    11
PRG="$(basename "$0")"
wenzelm
parents: 9789
diff changeset
    12
DIR="$(dirname "$0")"
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    13
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    14
function usage()
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    15
{
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    16
  echo
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    17
  echo "Usage: $PRG [OPTIONS]"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    18
  echo
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    19
  echo "  Options are:"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    20
  echo "    -h TEXT      head text"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    21
  echo "    -p           emit my pid"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    22
  echo "    -q           do not pipe stdin"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    23
  echo "    -t TEXT      tail text"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    24
  echo
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    25
  echo "  Output texts (pid, head, stdin, tail), then wait to be terminated."
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    26
  echo
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    27
  exit 1
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    28
}
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    29
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    30
function fail()
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    31
{
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    32
  echo "$1" >&2
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    33
  exit 2
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    34
}
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    35
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    36
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    37
## process command line
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    38
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    39
# options
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    40
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    41
HEAD=""
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    42
EMITPID=""
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    43
QUIT=""
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    44
TAIL=""
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    45
12111
d942348d8faf got rid of obsolete input filtering;
wenzelm
parents: 10555
diff changeset
    46
while getopts "h:pqt:" OPT
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    47
do
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    48
  case "$OPT" in
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    49
    h)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    50
      HEAD="$OPTARG"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    51
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    52
    p)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    53
      EMITPID=true
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    54
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    55
    q)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    56
      QUIT=true
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    57
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    58
    t)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    59
      TAIL="$OPTARG"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    60
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    61
    \?)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    62
      usage
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    63
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    64
  esac
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    65
done
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    66
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    67
shift $(($OPTIND - 1))
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    68
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    69
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    70
# args
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    71
9789
wenzelm
parents: 6082
diff changeset
    72
[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    73
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    74
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    75
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    76
## main
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    77
26576
fc76b7b79ba9 removed obsolete AUTO_PERL feature;
wenzelm
parents: 15847
diff changeset
    78
exec perl -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"