lib/Tools/logo

clarified "isabelle logo";

#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: create an instance of the Isabelle logo


PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] NAME"
  echo
  echo "  Create instance NAME of the Isabelle logo (as EPS or PDF)."
  echo
  echo "  Options are:"
  echo "    -o OUTPUT    specify output file and format (default \"isabelle_name.pdf\")"
  echo "    -q           quiet mode"
  echo
  exit 1
}

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


## process command line

# options

OUTPUT=""
QUIET=""

while getopts "o:q" OPT
do
  case "$OPT" in
    o)
      OUTPUT="$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 "$OUTPUT" ]; then
  OUTPUT=$(echo "$NAME" | tr A-Z a-z)
  [ -n "$OUTPUT" ] && OUTPUT="_${OUTPUT}"
  OUTPUT="isabelle${OUTPUT}.pdf"
  OUTPUT_FORMAT="pdf"
else
  case "$OUTPUT" in
    *.eps)
      OUTPUT_FORMAT="eps"
      ;;
    *.pdf)
      OUTPUT_FORMAT="pdf"
      ;;
    *)
      fail "Cannot guess output format (eps or pdf) from \"$OUTPUT\""
      ;;
  esac
fi

[ -z "$QUIET" ] && echo "$OUTPUT" >&2

if [ "$OUTPUT_FORMAT" = "eps" ]; then
  perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTPUT"
else
  perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" | \
    "$ISABELLE_EPSTOPDF" -f > "$OUTPUT"
fi