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