lib/Tools/logo
author wenzelm
Mon Aug 27 16:10:54 2012 +0200 (2012-08-27)
changeset 48936 e6d9e46ff7bc
parent 29143 72c960b2b83e
child 49072 747835eb2782
permissions -rwxr-xr-x
clarified "isabelle logo";
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@5557
     2
#
wenzelm@9788
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm@5557
     4
#
wenzelm@5557
     5
# DESCRIPTION: create an instance of the Isabelle logo
wenzelm@5557
     6
wenzelm@5557
     7
wenzelm@10511
     8
PRG="$(basename "$0")"
wenzelm@5557
     9
wenzelm@5557
    10
function usage()
wenzelm@5557
    11
{
wenzelm@5557
    12
  echo
wenzelm@28650
    13
  echo "Usage: isabelle $PRG [OPTIONS] NAME"
wenzelm@5570
    14
  echo
wenzelm@48936
    15
  echo "  Create instance NAME of the Isabelle logo (as EPS or PDF)."
wenzelm@5557
    16
  echo
wenzelm@5570
    17
  echo "  Options are:"
wenzelm@48936
    18
  echo "    -o OUTPUT    specify output file and format (default \"isabelle_name.pdf\")"
wenzelm@5570
    19
  echo "    -q           quiet mode"
wenzelm@5557
    20
  echo
wenzelm@5557
    21
  exit 1
wenzelm@5557
    22
}
wenzelm@5557
    23
wenzelm@5557
    24
function fail()
wenzelm@5557
    25
{
wenzelm@5557
    26
  echo "$1" >&2
wenzelm@5557
    27
  exit 2
wenzelm@5557
    28
}
wenzelm@5557
    29
wenzelm@5557
    30
wenzelm@5570
    31
## process command line
wenzelm@5570
    32
wenzelm@5570
    33
# options
wenzelm@5570
    34
wenzelm@48936
    35
OUTPUT=""
wenzelm@5570
    36
QUIET=""
wenzelm@5570
    37
wenzelm@5570
    38
while getopts "o:q" OPT
wenzelm@5570
    39
do
wenzelm@5570
    40
  case "$OPT" in
wenzelm@5570
    41
    o)
wenzelm@48936
    42
      OUTPUT="$OPTARG"
wenzelm@5570
    43
      ;;
wenzelm@5570
    44
    q)
wenzelm@5570
    45
      QUIET=true
wenzelm@5570
    46
      ;;
wenzelm@5570
    47
    \?)
wenzelm@5570
    48
      usage
wenzelm@5570
    49
      ;;
wenzelm@5570
    50
  esac
wenzelm@5570
    51
done
wenzelm@5570
    52
wenzelm@5570
    53
shift $(($OPTIND - 1))
wenzelm@5570
    54
wenzelm@5570
    55
wenzelm@5570
    56
# args
wenzelm@5557
    57
wenzelm@5587
    58
NAME="-"
wenzelm@9788
    59
[ "$#" -ge 1 ] && { NAME="$1"; shift; }
wenzelm@5557
    60
wenzelm@9788
    61
[ "$#" -ne 0 -o "$NAME" = "-" ] && usage
wenzelm@5557
    62
wenzelm@5557
    63
wenzelm@5557
    64
## main
wenzelm@5557
    65
wenzelm@48936
    66
if [ -z "$OUTPUT" ]; then
wenzelm@48936
    67
  OUTPUT=$(echo "$NAME" | tr A-Z a-z)
wenzelm@48936
    68
  [ -n "$OUTPUT" ] && OUTPUT="_${OUTPUT}"
wenzelm@48936
    69
  OUTPUT="isabelle${OUTPUT}.pdf"
wenzelm@48936
    70
  OUTPUT_FORMAT="pdf"
wenzelm@48936
    71
else
wenzelm@48936
    72
  case "$OUTPUT" in
wenzelm@48936
    73
    *.eps)
wenzelm@48936
    74
      OUTPUT_FORMAT="eps"
wenzelm@48936
    75
      ;;
wenzelm@48936
    76
    *.pdf)
wenzelm@48936
    77
      OUTPUT_FORMAT="pdf"
wenzelm@48936
    78
      ;;
wenzelm@48936
    79
    *)
wenzelm@48936
    80
      fail "Cannot guess output format (eps or pdf) from \"$OUTPUT\""
wenzelm@48936
    81
      ;;
wenzelm@48936
    82
  esac
wenzelm@5570
    83
fi
wenzelm@5570
    84
wenzelm@48936
    85
[ -z "$QUIET" ] && echo "$OUTPUT" >&2
wenzelm@48936
    86
wenzelm@48936
    87
if [ "$OUTPUT_FORMAT" = "eps" ]; then
wenzelm@48936
    88
  perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTPUT"
wenzelm@5570
    89
else
wenzelm@48936
    90
  perl -p -e "s,<any>,$NAME," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" | \
wenzelm@48936
    91
    "$ISABELLE_EPSTOPDF" -f > "$OUTPUT"
wenzelm@5570
    92
fi