lib/Tools/logo
author hoelzl
Mon, 06 Dec 2010 19:54:48 +0100
changeset 41024 ba961a606c67
parent 29143 72c960b2b83e
child 48936 e6d9e46ff7bc
permissions -rwxr-xr-x
move coercions to appropriate places
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
#
9788
wenzelm
parents: 6082
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
5557
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
10511
wenzelm
parents: 9788
diff changeset
     8
PRG="$(basename "$0")"
5557
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
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 26576
diff changeset
    13
  echo "Usage: isabelle $PRG [OPTIONS] NAME"
5570
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="-"
9788
wenzelm
parents: 6082
diff changeset
    59
[ "$#" -ge 1 ] && { NAME="$1"; shift; }
5557
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    60
9788
wenzelm
parents: 6082
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
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    72
if [ "$OUTFILE" = "-" ]; then
26576
fc76b7b79ba9 removed obsolete AUTO_PERL feature;
wenzelm
parents: 15847
diff changeset
    73
  perl -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps"
5570
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    74
else
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    75
  [ -z "$QUIET" ] && echo "$OUTFILE" >&2
26576
fc76b7b79ba9 removed obsolete AUTO_PERL feature;
wenzelm
parents: 15847
diff changeset
    76
  perl -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE"
5570
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    77
fi