lib/Tools/logo
author wenzelm
Tue, 12 Jan 1999 12:17:53 +0100
changeset 6082 590f9e3bf4d8
parent 5587 7fceb6eea475
child 9788 df671fa2562a
permissions -rwxr-xr-x
configure AUTO_BASH, AUTO_PERL;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5557
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
     1
#!/bin/bash
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
     2
#
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
     3
# $Id$
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
     4
#
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: create an instance of the Isabelle logo
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
     6
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
     7
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
     8
PRG=$(basename $0)
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
     9
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    10
function usage()
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    11
{
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    12
  echo
5570
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    13
  echo "Usage: $PRG [OPTIONS] NAME"
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    14
  echo
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    15
  echo "  Create instance NAME of the Isabelle logo (as EPS)."
5557
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    16
  echo
5570
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    17
  echo "  Options are:"
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    18
  echo "    -o OUTFILE   set output file (default determined from NAME)"
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    19
  echo "    -q           quiet mode"
5557
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    20
  echo
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    21
  exit 1
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    22
}
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    23
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    24
function fail()
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    25
{
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    26
  echo "$1" >&2
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    27
  exit 2
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    28
}
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    29
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    30
5570
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    31
## process command line
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    32
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    33
# options
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    34
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    35
OUTFILE=""
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    36
QUIET=""
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    37
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    38
while getopts "o:q" OPT
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    39
do
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    40
  case "$OPT" in
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    41
    o)
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    42
      OUTFILE="$OPTARG"
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    43
      ;;
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    44
    q)
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    45
      QUIET=true
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    46
      ;;
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    47
    \?)
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    48
      usage
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    49
      ;;
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    50
  esac
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    51
done
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    52
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    53
shift $(($OPTIND - 1))
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    54
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    55
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    56
# args
5557
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    57
5587
7fceb6eea475 handle empty name;
wenzelm
parents: 5570
diff changeset
    58
NAME="-"
5557
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    59
[ $# -ge 1 ] && { NAME="$1"; shift; }
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    60
5587
7fceb6eea475 handle empty name;
wenzelm
parents: 5570
diff changeset
    61
[ $# -ne 0 -o "$NAME" = "-" ] && usage
5557
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    62
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    63
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    64
## main
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    65
5570
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    66
if [ -z "$OUTFILE" ]; then
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    67
  OUTFILE=$(echo "$NAME" | tr A-Z a-z)
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    68
  [ -n "$OUTFILE" ] && OUTFILE="_$OUTFILE"
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    69
  OUTFILE="isabelle${OUTFILE}.eps"
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    70
fi
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    71
6082
590f9e3bf4d8 configure AUTO_BASH, AUTO_PERL;
wenzelm
parents: 5587
diff changeset
    72
#set by configure
590f9e3bf4d8 configure AUTO_BASH, AUTO_PERL;
wenzelm
parents: 5587
diff changeset
    73
AUTO_PERL=perl
590f9e3bf4d8 configure AUTO_BASH, AUTO_PERL;
wenzelm
parents: 5587
diff changeset
    74
5570
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    75
if [ "$OUTFILE" = "-" ]; then
6082
590f9e3bf4d8 configure AUTO_BASH, AUTO_PERL;
wenzelm
parents: 5587
diff changeset
    76
  $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
5570
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    77
else
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    78
  [ -z "$QUIET" ] && echo "$OUTFILE" >&2
6082
590f9e3bf4d8 configure AUTO_BASH, AUTO_PERL;
wenzelm
parents: 5587
diff changeset
    79
  $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
5570
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    80
fi