lib/scripts/feeder
author wenzelm
Tue, 21 Nov 2006 18:07:33 +0100
changeset 21437 a3c55b85cf0e
parent 15847 c05c7670f166
child 26576 fc76b7b79ba9
permissions -rwxr-xr-x
moved theorem kinds from PureThy to Thm;
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
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     5
#
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     6
# feeder - feed isabelle session
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     7
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     8
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     9
## diagnostics
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    10
10512
wenzelm
parents: 9789
diff changeset
    11
PRG="$(basename "$0")"
wenzelm
parents: 9789
diff changeset
    12
DIR="$(dirname "$0")"
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    13
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    14
function usage()
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    15
{
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    16
  echo
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    17
  echo "Usage: $PRG [OPTIONS]"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    18
  echo
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    19
  echo "  Options are:"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    20
  echo "    -h TEXT      head text"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    21
  echo "    -p           emit my pid"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    22
  echo "    -q           do not pipe stdin"
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
TAIL=""
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    45
12111
d942348d8faf got rid of obsolete input filtering;
wenzelm
parents: 10555
diff changeset
    46
while getopts "h:pqt:" OPT
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    47
do
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    48
  case "$OPT" in
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    49
    h)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    50
      HEAD="$OPTARG"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    51
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    52
    p)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    53
      EMITPID=true
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    54
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    55
    q)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    56
      QUIT=true
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    57
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    58
    t)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    59
      TAIL="$OPTARG"
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    60
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    61
    \?)
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    62
      usage
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    63
      ;;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    64
  esac
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    65
done
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    66
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    67
shift $(($OPTIND - 1))
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    68
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    69
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    70
# args
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    71
9789
wenzelm
parents: 6082
diff changeset
    72
[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    73
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
## main
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    77
6082
590f9e3bf4d8 configure AUTO_BASH, AUTO_PERL;
wenzelm
parents: 4504
diff changeset
    78
#set by configure
15847
c05c7670f166 restored AUTO_BASH/PERL -- beware of ./configure!
wenzelm
parents: 14981
diff changeset
    79
AUTO_PERL=perl
6082
590f9e3bf4d8 configure AUTO_BASH, AUTO_PERL;
wenzelm
parents: 4504
diff changeset
    80
12111
d942348d8faf got rid of obsolete input filtering;
wenzelm
parents: 10555
diff changeset
    81
exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"