improved;
authorwenzelm
Fri Sep 25 14:32:36 1998 +0200 (1998-09-25)
changeset 5570ae1b56ef16b0
parent 5569 8c7e1190e789
child 5571 3613c5d22cc6
improved;
lib/Tools/logo
     1.1 --- a/lib/Tools/logo	Fri Sep 25 14:06:56 1998 +0200
     1.2 +++ b/lib/Tools/logo	Fri Sep 25 14:32:36 1998 +0200
     1.3 @@ -10,9 +10,13 @@
     1.4  function usage()
     1.5  {
     1.6    echo
     1.7 -  echo "Usage: $PRG NAME"
     1.8 +  echo "Usage: $PRG [OPTIONS] NAME"
     1.9 +  echo
    1.10 +  echo "  Create instance NAME of the Isabelle logo (as EPS)."
    1.11    echo
    1.12 -  echo "  Create instance NAME of the Isabelle logo (as EPS to stdout)."
    1.13 +  echo "  Options are:"
    1.14 +  echo "    -o OUTFILE   set output file (default determined from NAME)"
    1.15 +  echo "    -q           quiet mode"
    1.16    echo
    1.17    exit 1
    1.18  }
    1.19 @@ -24,14 +28,50 @@
    1.20  }
    1.21  
    1.22  
    1.23 -## args
    1.24 +## process command line
    1.25 +
    1.26 +# options
    1.27 +
    1.28 +OUTFILE=""
    1.29 +QUIET=""
    1.30 +
    1.31 +while getopts "o:q" OPT
    1.32 +do
    1.33 +  case "$OPT" in
    1.34 +    o)
    1.35 +      OUTFILE="$OPTARG"
    1.36 +      ;;
    1.37 +    q)
    1.38 +      QUIET=true
    1.39 +      ;;
    1.40 +    \?)
    1.41 +      usage
    1.42 +      ;;
    1.43 +  esac
    1.44 +done
    1.45 +
    1.46 +shift $(($OPTIND - 1))
    1.47 +
    1.48 +
    1.49 +# args
    1.50  
    1.51  NAME=""
    1.52  [ $# -ge 1 ] && { NAME="$1"; shift; }
    1.53  
    1.54 -[ $# -ne 0 -o "$NAME" = "-?" -o -z "$NAME" ] && usage
    1.55 +[ $# -ne 0 -o -z "$NAME" ] && usage
    1.56  
    1.57  
    1.58  ## main
    1.59  
    1.60 -perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
    1.61 +if [ -z "$OUTFILE" ]; then
    1.62 +  OUTFILE=$(echo "$NAME" | tr A-Z a-z)
    1.63 +  [ -n "$OUTFILE" ] && OUTFILE="_$OUTFILE"
    1.64 +  OUTFILE="isabelle${OUTFILE}.eps"
    1.65 +fi
    1.66 +
    1.67 +if [ "$OUTFILE" = "-" ]; then
    1.68 +  perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
    1.69 +else
    1.70 +  [ -z "$QUIET" ] && echo "$OUTFILE" >&2
    1.71 +  perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
    1.72 +fi