lib/Tools/logo

unused (see 29566b6810f7);

#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: create an instance of the Isabelle logo (PDF)


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

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] [XYZ]"
  echo
  echo "  Create instance XYZ of the Isabelle logo (PDF)."
  echo
  echo "  Options are:"
  echo "    -o FILE      alternative output file (default \"isabelle_xyx.pdf\")"
  echo "    -q           quiet mode"
  echo
  exit 1
}

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


## process command line

# options

OUTPUT_FILE=""
QUIET=""

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

shift $(($OPTIND - 1))


# args

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

[ "$#" -ne 0 ] && usage


## main

if [ -z "$OUTPUT_FILE" ]; then
  OUTPUT_NAME="$(echo "$TEXT" | tr A-Z a-z)"
  if [ -z "$OUTPUT_NAME" ]; then
    OUTPUT_FILE="isabelle.pdf"
  else
    OUTPUT_FILE="isabelle_${OUTPUT_NAME}.pdf"
  fi
fi

[ -z "$QUIET" ] && echo "$OUTPUT_FILE" >&2
perl -p -e "s,<any>,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" | \
  "$ISABELLE_EPSTOPDF" --filter > "$OUTPUT_FILE"