equal
deleted
inserted
replaced
|
1 #!/bin/bash |
|
2 # |
|
3 # $Id$ |
|
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" |
|
20 echo " -i ignore INT signal" |
|
21 echo " -p emit my pid" |
|
22 echo " -q do not pipe stdin" |
|
23 echo " -s filter symbols" |
|
24 echo " -t TEXT tail text" |
|
25 echo |
|
26 echo " Output texts (pid, head, stdin, tail), then wait to be terminated." |
|
27 echo |
|
28 exit 1 |
|
29 } |
|
30 |
|
31 function fail() |
|
32 { |
|
33 echo "$1" >&2 |
|
34 exit 2 |
|
35 } |
|
36 |
|
37 |
|
38 ## process command line |
|
39 |
|
40 # options |
|
41 |
|
42 HEAD="" |
|
43 NOINT="" |
|
44 EMITPID="" |
|
45 QUIT="" |
|
46 SYMBOLS="" |
|
47 TAIL="" |
|
48 |
|
49 while getopts "h:ipqst:" OPT |
|
50 do |
|
51 case "$OPT" in |
|
52 h) |
|
53 HEAD="$OPTARG" |
|
54 ;; |
|
55 i) |
|
56 NOINT=true |
|
57 ;; |
|
58 p) |
|
59 EMITPID=true |
|
60 ;; |
|
61 q) |
|
62 QUIT=true |
|
63 ;; |
|
64 s) |
|
65 SYMBOLS=true |
|
66 ;; |
|
67 t) |
|
68 TAIL="$OPTARG" |
|
69 ;; |
|
70 \?) |
|
71 usage |
|
72 ;; |
|
73 esac |
|
74 done |
|
75 |
|
76 shift $(($OPTIND - 1)) |
|
77 |
|
78 |
|
79 # args |
|
80 |
|
81 [ $# -ne 0 ] && { echo "Bad args: $*"; usage; } |
|
82 |
|
83 |
|
84 |
|
85 ## main |
|
86 |
|
87 exec perl -w $DIR/feeder.pl "$HEAD" "$NOINT" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL" |