| 
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
  |