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