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