# HG changeset patch
# User wenzelm
# Date 906726756 -7200
# Node ID ae1b56ef16b0c6a52d201ef79f3d6feef31438c3
# Parent  8c7e1190e789cb36e493eee8321d03ac38f05e5e
improved;

diff -r 8c7e1190e789 -r ae1b56ef16b0 lib/Tools/logo
--- a/lib/Tools/logo	Fri Sep 25 14:06:56 1998 +0200
+++ b/lib/Tools/logo	Fri Sep 25 14:32:36 1998 +0200
@@ -10,9 +10,13 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG NAME"
+  echo "Usage: $PRG [OPTIONS] NAME"
+  echo
+  echo "  Create instance NAME of the Isabelle logo (as EPS)."
   echo
-  echo "  Create instance NAME of the Isabelle logo (as EPS to stdout)."
+  echo "  Options are:"
+  echo "    -o OUTFILE   set output file (default determined from NAME)"
+  echo "    -q           quiet mode"
   echo
   exit 1
 }
@@ -24,14 +28,50 @@
 }
 
 
-## args
+## 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" = "-?" -o -z "$NAME" ] && usage
+[ $# -ne 0 -o -z "$NAME" ] && usage
 
 
 ## main
 
-perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
+if [ -z "$OUTFILE" ]; then
+  OUTFILE=$(echo "$NAME" | tr A-Z a-z)
+  [ -n "$OUTFILE" ] && OUTFILE="_$OUTFILE"
+  OUTFILE="isabelle${OUTFILE}.eps"
+fi
+
+if [ "$OUTFILE" = "-" ]; then
+  perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
+else
+  [ -z "$QUIET" ] && echo "$OUTFILE" >&2
+  perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
+fi