lib/Tools/logo

backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;

#!/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] [XYZ]"
  echo
  echo "  Create instance XYZ of the Isabelle logo (as EPS and PDF)."
  echo
  echo "  Options are:"
  echo "    -n NAME      alternative output base name (default \"isabelle_xyx\")"
  echo "    -q           quiet mode"
  echo
  exit 1
}

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


## process command line

# options

OUTPUT_NAME=""
QUIET=""

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

shift $(($OPTIND - 1))


# args

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

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


## main

case "$OUTPUT_NAME" in
  "")
    OUTPUT_NAME=$(echo "$TEXT" | tr A-Z a-z)
    if [ -z "$OUTPUT_NAME" ]; then
      OUTPUT_NAME="isabelle"
    else
      OUTPUT_NAME="isabelle_${OUTPUT_NAME}"
    fi
    ;;
  */* | *.eps | *.pdf)
    fail "Bad output base name: \"$OUTPUT_NAME\""
    ;;
  *)
    ;;
esac

[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.eps" >&2
perl -p -e "s,<any>,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps"

[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.pdf" >&2
"$ISABELLE_EPSTOPDF" "${OUTPUT_NAME}.eps"