lib/Tools/logo

GPLed;
more robust handling of spaces in args / file names;

#!/bin/bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# DESCRIPTION: create an instance of the Isabelle logo


PRG=$(basename "$0")

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] NAME"
  echo
  echo "  Create instance NAME of the Isabelle logo (as EPS)."
  echo
  echo "  Options are:"
  echo "    -o OUTFILE   set output file (default determined from NAME)"
  echo "    -q           quiet mode"
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

OUTFILE=""
QUIET=""

while getopts "o:q" OPT
do
  case "$OPT" in
    o)
      OUTFILE="$OPTARG"
      ;;
    q)
      QUIET=true
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

NAME="-"
[ "$#" -ge 1 ] && { NAME="$1"; shift; }

[ "$#" -ne 0 -o "$NAME" = "-" ] && usage


## main

if [ -z "$OUTFILE" ]; then
  OUTFILE=$(echo "$NAME" | tr A-Z a-z)
  [ -n "$OUTFILE" ] && OUTFILE="_$OUTFILE"
  OUTFILE="isabelle${OUTFILE}.eps"
fi

#set by configure
AUTO_PERL=perl

if [ "$OUTFILE" = "-" ]; then
  "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps"
else
  [ -z "$QUIET" ] && echo "$OUTFILE" >&2
  "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE"
fi