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