lib/Tools/logo
author paulson
Tue, 10 Feb 2004 12:02:11 +0100
changeset 14378 69c4d5997669
parent 10555 2323ec838401
child 14981 e73f8140af78
permissions -rwxr-xr-x
generic of_nat and of_int functions, and generalization of iszero and neg

#!/usr/bin/env 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