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