equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
|
2 # |
|
3 # Author: Markus Wenzel, TU Muenchen |
|
4 # |
|
5 # feeder - feed isabelle session |
|
6 |
|
7 |
|
8 ## diagnostics |
|
9 |
|
10 PRG="$(basename "$0")" |
|
11 DIR="$(dirname "$0")" |
|
12 |
|
13 function usage() |
|
14 { |
|
15 echo |
|
16 echo "Usage: $PRG [OPTIONS]" |
|
17 echo |
|
18 echo " Options are:" |
|
19 echo " -h TEXT head text (encoded as utf8)" |
|
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 |
|
45 while getopts "h:pqt:" OPT |
|
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 |
|
71 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; } |
|
72 |
|
73 |
|
74 |
|
75 ## main |
|
76 |
|
77 exec perl -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL" |
|