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;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # DESCRIPTION: create an instance of the Isabelle logo
     6 
     7 
     8 PRG=$(basename $0)
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: $PRG [OPTIONS] NAME"
    14   echo
    15   echo "  Create instance NAME of the Isabelle logo (as EPS)."
    16   echo
    17   echo "  Options are:"
    18   echo "    -o OUTFILE   set output file (default determined from NAME)"
    19   echo "    -q           quiet mode"
    20   echo
    21   exit 1
    22 }
    23 
    24 function fail()
    25 {
    26   echo "$1" >&2
    27   exit 2
    28 }
    29 
    30 
    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
    57 
    58 NAME="-"
    59 [ $# -ge 1 ] && { NAME="$1"; shift; }
    60 
    61 [ $# -ne 0 -o "$NAME" = "-" ] && usage
    62 
    63 
    64 ## main
    65 
    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
    73   perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
    74 else
    75   [ -z "$QUIET" ] && echo "$OUTFILE" >&2
    76   perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
    77 fi