author | bulwahn |
Tue, 06 Dec 2011 15:23:16 +0100 | |
changeset 45773 | 7f2366dc8c0f |
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" |