lib/scripts/feeder
author wenzelm
Tue, 13 Feb 2001 16:31:18 +0100
changeset 11109 ce1cefc6c14c
parent 10555 2323ec838401
child 12111 d942348d8faf
permissions -rwxr-xr-x
tuned;
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
wenzelm
parents: 6082
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     6
#
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     7
# feeder - feed isabelle session
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     8
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     9
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    10
## diagnostics
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    11
10512
wenzelm
parents: 9789
diff changeset
    12
PRG="$(basename "$0")"
wenzelm
parents: 9789
diff changeset
    13
DIR="$(dirname "$0")"
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    14
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    15
function usage()
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    16
{
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    17
  echo
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    18
  echo "Usage: $PRG [OPTIONS]"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    19
  echo
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    20
  echo "  Options are:"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    21
  echo "    -h TEXT      head text"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    22
  echo "    -p           emit my pid"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    23
  echo "    -q           do not pipe stdin"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    24
  echo "    -s           filter symbols"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    25
  echo "    -t TEXT      tail text"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    26
  echo
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    27
  echo "  Output texts (pid, head, stdin, tail), then wait to be terminated."
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    28
  echo
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    29
  exit 1
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    30
}
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    31
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    32
function fail()
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    33
{
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    34
  echo "$1" >&2
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    35
  exit 2
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    36
}
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    37
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    38
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    39
## process command line
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    40
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    41
# options
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    42
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    43
HEAD=""
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    44
EMITPID=""
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    45
QUIT=""
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    46
SYMBOLS=""
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    47
TAIL=""
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    48
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
    49
while getopts "h:pqst:" OPT
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    50
do
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    51
  case "$OPT" in
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    52
    h)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    53
      HEAD="$OPTARG"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    54
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    55
    p)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    56
      EMITPID=true
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    57
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    58
    q)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    59
      QUIT=true
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    60
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    61
    s)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    62
      SYMBOLS=true
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    63
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    64
    t)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    65
      TAIL="$OPTARG"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    66
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    67
    \?)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    68
      usage
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    69
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    70
  esac
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    71
done
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    72
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    73
shift $(($OPTIND - 1))
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
# args
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    77
9789
wenzelm
parents: 6082
diff changeset
    78
[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    79
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    80
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    81
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    82
## main
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    83
6082
590f9e3bf4d8 configure AUTO_BASH, AUTO_PERL;
wenzelm
parents: 4504
diff changeset
    84
#set by configure
590f9e3bf4d8 configure AUTO_BASH, AUTO_PERL;
wenzelm
parents: 4504
diff changeset
    85
AUTO_PERL=perl
590f9e3bf4d8 configure AUTO_BASH, AUTO_PERL;
wenzelm
parents: 4504
diff changeset
    86
9789
wenzelm
parents: 6082
diff changeset
    87
exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"