lib/scripts/feeder
author wenzelm
Fri, 13 Mar 1998 18:15:14 +0100
changeset 4744 4469d498cd48
parent 4504 2f39aa4bebf3
child 6082 590f9e3bf4d8
permissions -rwxr-xr-x
moved addsplits [expand_if] from HOL_basic_ss to HOL_ss;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     1
#!/bin/bash
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     2
#
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     3
# $Id$
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     4
#
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     5
# feeder - feed isabelle session
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     6
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     7
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     8
## diagnostics
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     9
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    10
PRG=$(basename $0)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    11
DIR=$(dirname $0)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    12
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    13
function usage()
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    14
{
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    15
  echo
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    16
  echo "Usage: $PRG [OPTIONS]"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    17
  echo
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    18
  echo "  Options are:"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    19
  echo "    -h TEXT      head text"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    20
  echo "    -p           emit my pid"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    21
  echo "    -q           do not pipe stdin"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    22
  echo "    -s           filter symbols"
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
SYMBOLS=""
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    45
TAIL=""
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    46
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
    47
while getopts "h:pqst:" OPT
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    48
do
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    49
  case "$OPT" in
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    50
    h)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    51
      HEAD="$OPTARG"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    52
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    53
    p)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    54
      EMITPID=true
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    55
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    56
    q)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    57
      QUIT=true
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    58
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    59
    s)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    60
      SYMBOLS=true
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    61
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    62
    t)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    63
      TAIL="$OPTARG"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    64
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    65
    \?)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    66
      usage
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    67
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    68
  esac
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    69
done
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    70
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    71
shift $(($OPTIND - 1))
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    72
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    73
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    74
# args
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    75
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    76
[ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    77
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    78
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    79
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    80
## main
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    81
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
    82
exec perl -w $DIR/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"