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