#!/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,,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps" [ -z "$QUIET" ] && echo "${OUTPUT_NAME}.pdf" >&2 "$ISABELLE_EPSTOPDF" "${OUTPUT_NAME}.eps"