#!/bin/sh # # $Id: logo,v 1.10 2005/04/26 17:50:58 wenzelm Exp $ # Author: Markus Wenzel, TU Muenchen # # DESCRIPTION: create an instance of the Isabelle logo PRG="$(basename "$0")" 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 } 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 #set by configure AUTO_PERL=perl if [ "$OUTFILE" = "-" ]; then "$AUTO_PERL" -p -e "s//$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" else [ -z "$QUIET" ] && echo "$OUTFILE" >&2 "$AUTO_PERL" -p -e "s//$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE" fi