| author | paulson | 
| Wed, 10 Oct 2007 15:05:34 +0200 | |
| changeset 24942 | 39a23aadc7e1 | 
| 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: 
15574diff
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 |