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