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