lib/Tools/logo

remove unused lemmas ub2ub_monofun' and dir2dir_monofun

#!/usr/bin/env bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# 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

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