lib/Tools/logo
changeset 5570 ae1b56ef16b0
parent 5557 d6ceb4275742
child 5587 7fceb6eea475
equal deleted inserted replaced
5569:8c7e1190e789 5570:ae1b56ef16b0
     8 PRG=$(basename $0)
     8 PRG=$(basename $0)
     9 
     9 
    10 function usage()
    10 function usage()
    11 {
    11 {
    12   echo
    12   echo
    13   echo "Usage: $PRG NAME"
    13   echo "Usage: $PRG [OPTIONS] NAME"
    14   echo
    14   echo
    15   echo "  Create instance NAME of the Isabelle logo (as EPS to stdout)."
    15   echo "  Create instance NAME of the Isabelle logo (as EPS)."
       
    16   echo
       
    17   echo "  Options are:"
       
    18   echo "    -o OUTFILE   set output file (default determined from NAME)"
       
    19   echo "    -q           quiet mode"
    16   echo
    20   echo
    17   exit 1
    21   exit 1
    18 }
    22 }
    19 
    23 
    20 function fail()
    24 function fail()
    22   echo "$1" >&2
    26   echo "$1" >&2
    23   exit 2
    27   exit 2
    24 }
    28 }
    25 
    29 
    26 
    30 
    27 ## args
    31 ## process command line
       
    32 
       
    33 # options
       
    34 
       
    35 OUTFILE=""
       
    36 QUIET=""
       
    37 
       
    38 while getopts "o:q" OPT
       
    39 do
       
    40   case "$OPT" in
       
    41     o)
       
    42       OUTFILE="$OPTARG"
       
    43       ;;
       
    44     q)
       
    45       QUIET=true
       
    46       ;;
       
    47     \?)
       
    48       usage
       
    49       ;;
       
    50   esac
       
    51 done
       
    52 
       
    53 shift $(($OPTIND - 1))
       
    54 
       
    55 
       
    56 # args
    28 
    57 
    29 NAME=""
    58 NAME=""
    30 [ $# -ge 1 ] && { NAME="$1"; shift; }
    59 [ $# -ge 1 ] && { NAME="$1"; shift; }
    31 
    60 
    32 [ $# -ne 0 -o "$NAME" = "-?" -o -z "$NAME" ] && usage
    61 [ $# -ne 0 -o -z "$NAME" ] && usage
    33 
    62 
    34 
    63 
    35 ## main
    64 ## main
    36 
    65 
    37 perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
    66 if [ -z "$OUTFILE" ]; then
       
    67   OUTFILE=$(echo "$NAME" | tr A-Z a-z)
       
    68   [ -n "$OUTFILE" ] && OUTFILE="_$OUTFILE"
       
    69   OUTFILE="isabelle${OUTFILE}.eps"
       
    70 fi
       
    71 
       
    72 if [ "$OUTFILE" = "-" ]; then
       
    73   perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
       
    74 else
       
    75   [ -z "$QUIET" ] && echo "$OUTFILE" >&2
       
    76   perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
       
    77 fi