| author | bulwahn | 
| Sat, 09 Jul 2011 19:28:33 +0200 | |
| changeset 43733 | a6ca7b83612f | 
| parent 40335 | 3e4bb6e7c3ca | 
| permissions | -rwxr-xr-x | 
| 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:"  | 
|
| 
40335
 
3e4bb6e7c3ca
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
 
wenzelm 
parents: 
29145 
diff
changeset
 | 
19  | 
echo " -h TEXT head text (encoded as utf8)"  | 
| 4501 | 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"  |