| author | haftmann | 
| Fri, 20 Apr 2007 11:21:39 +0200 | |
| changeset 22741 | 4bd02e03305c | 
| parent 15847 | c05c7670f166 | 
| child 26576 | fc76b7b79ba9 | 
| permissions | -rwxr-xr-x | 
| 10555 | 1  | 
#!/usr/bin/env bash  | 
| 5557 | 2  | 
#  | 
3  | 
# $Id$  | 
|
| 9788 | 4  | 
# Author: Markus Wenzel, TU Muenchen  | 
| 5557 | 5  | 
#  | 
6  | 
# DESCRIPTION: create an instance of the Isabelle logo  | 
|
7  | 
||
8  | 
||
| 10511 | 9  | 
PRG="$(basename "$0")"  | 
| 5557 | 10  | 
|
11  | 
function usage()  | 
|
12  | 
{
 | 
|
13  | 
echo  | 
|
| 5570 | 14  | 
echo "Usage: $PRG [OPTIONS] NAME"  | 
15  | 
echo  | 
|
16  | 
echo " Create instance NAME of the Isabelle logo (as EPS)."  | 
|
| 5557 | 17  | 
echo  | 
| 5570 | 18  | 
echo " Options are:"  | 
19  | 
echo " -o OUTFILE set output file (default determined from NAME)"  | 
|
20  | 
echo " -q quiet mode"  | 
|
| 5557 | 21  | 
echo  | 
22  | 
exit 1  | 
|
23  | 
}  | 
|
24  | 
||
25  | 
function fail()  | 
|
26  | 
{
 | 
|
27  | 
echo "$1" >&2  | 
|
28  | 
exit 2  | 
|
29  | 
}  | 
|
30  | 
||
31  | 
||
| 5570 | 32  | 
## process command line  | 
33  | 
||
34  | 
# options  | 
|
35  | 
||
36  | 
OUTFILE=""  | 
|
37  | 
QUIET=""  | 
|
38  | 
||
39  | 
while getopts "o:q" OPT  | 
|
40  | 
do  | 
|
41  | 
case "$OPT" in  | 
|
42  | 
o)  | 
|
43  | 
OUTFILE="$OPTARG"  | 
|
44  | 
;;  | 
|
45  | 
q)  | 
|
46  | 
QUIET=true  | 
|
47  | 
;;  | 
|
48  | 
\?)  | 
|
49  | 
usage  | 
|
50  | 
;;  | 
|
51  | 
esac  | 
|
52  | 
done  | 
|
53  | 
||
54  | 
shift $(($OPTIND - 1))  | 
|
55  | 
||
56  | 
||
57  | 
# args  | 
|
| 5557 | 58  | 
|
| 5587 | 59  | 
NAME="-"  | 
| 9788 | 60  | 
[ "$#" -ge 1 ] && { NAME="$1"; shift; }
 | 
| 5557 | 61  | 
|
| 9788 | 62  | 
[ "$#" -ne 0 -o "$NAME" = "-" ] && usage  | 
| 5557 | 63  | 
|
64  | 
||
65  | 
## main  | 
|
66  | 
||
| 5570 | 67  | 
if [ -z "$OUTFILE" ]; then  | 
68  | 
OUTFILE=$(echo "$NAME" | tr A-Z a-z)  | 
|
69  | 
[ -n "$OUTFILE" ] && OUTFILE="_$OUTFILE"  | 
|
70  | 
  OUTFILE="isabelle${OUTFILE}.eps"
 | 
|
71  | 
fi  | 
|
72  | 
||
| 6082 | 73  | 
#set by configure  | 
| 
15847
 
c05c7670f166
restored AUTO_BASH/PERL -- beware of ./configure!
 
wenzelm 
parents: 
15574 
diff
changeset
 | 
74  | 
AUTO_PERL=perl  | 
| 6082 | 75  | 
|
| 5570 | 76  | 
if [ "$OUTFILE" = "-" ]; then  | 
| 9788 | 77  | 
"$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps"  | 
| 5570 | 78  | 
else  | 
79  | 
[ -z "$QUIET" ] && echo "$OUTFILE" >&2  | 
|
| 9788 | 80  | 
"$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE"  | 
| 5570 | 81  | 
fi  |