| 10555 |      1 | #!/usr/bin/env bash
 | 
| 4501 |      2 | #
 | 
| 9789 |      3 | # Author: Markus Wenzel, TU Muenchen
 | 
| 4501 |      4 | #
 | 
|  |      5 | # feeder - feed isabelle session
 | 
|  |      6 | 
 | 
|  |      7 | 
 | 
|  |      8 | ## diagnostics
 | 
|  |      9 | 
 | 
| 10512 |     10 | PRG="$(basename "$0")"
 | 
|  |     11 | DIR="$(dirname "$0")"
 | 
| 4501 |     12 | 
 | 
|  |     13 | function usage()
 | 
|  |     14 | {
 | 
|  |     15 |   echo
 | 
|  |     16 |   echo "Usage: $PRG [OPTIONS]"
 | 
|  |     17 |   echo
 | 
|  |     18 |   echo "  Options are:"
 | 
|  |     19 |   echo "    -h TEXT      head text"
 | 
|  |     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 | 
 | 
| 12111 |     45 | while getopts "h:pqt:" OPT
 | 
| 4501 |     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 | 
 | 
| 9789 |     71 | [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
 | 
| 4501 |     72 | 
 | 
|  |     73 | 
 | 
|  |     74 | 
 | 
|  |     75 | ## main
 | 
|  |     76 | 
 | 
| 26576 |     77 | exec perl -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"
 |