lib/Tools/logo
author wenzelm
Thu Apr 24 00:29:55 2014 +0200 (2014-04-24)
changeset 56686 2386d1a3ca8f
parent 53774 729a43c36ccb
permissions -rwxr-xr-x
canonical list operations, as in ML;
avoid odd mutable data structures;
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@49072
    13
  echo "Usage: isabelle $PRG [OPTIONS] [XYZ]"
wenzelm@5570
    14
  echo
wenzelm@49072
    15
  echo "  Create instance XYZ of the Isabelle logo (as EPS and PDF)."
wenzelm@5557
    16
  echo
wenzelm@5570
    17
  echo "  Options are:"
wenzelm@49072
    18
  echo "    -n NAME      alternative output base name (default \"isabelle_xyx\")"
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@49072
    35
OUTPUT_NAME=""
wenzelm@5570
    36
QUIET=""
wenzelm@5570
    37
wenzelm@49072
    38
while getopts "n:q" OPT
wenzelm@5570
    39
do
wenzelm@5570
    40
  case "$OPT" in
wenzelm@49072
    41
    n)
wenzelm@49072
    42
      OUTPUT_NAME="$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@49072
    58
TEXT=""
wenzelm@49072
    59
[ "$#" -ge 1 ] && { TEXT="$1"; shift; }
wenzelm@5557
    60
wenzelm@49072
    61
[ "$#" -ne 0 ] && usage
wenzelm@5557
    62
wenzelm@5557
    63
wenzelm@5557
    64
## main
wenzelm@5557
    65
wenzelm@49072
    66
case "$OUTPUT_NAME" in
wenzelm@49072
    67
  "")
wenzelm@49072
    68
    OUTPUT_NAME=$(echo "$TEXT" | tr A-Z a-z)
wenzelm@49072
    69
    if [ -z "$OUTPUT_NAME" ]; then
wenzelm@49072
    70
      OUTPUT_NAME="isabelle"
wenzelm@49072
    71
    else
wenzelm@49072
    72
      OUTPUT_NAME="isabelle_${OUTPUT_NAME}"
wenzelm@49072
    73
    fi
wenzelm@49072
    74
    ;;
wenzelm@49072
    75
  */* | *.eps | *.pdf)
wenzelm@49072
    76
    fail "Bad output base name: \"$OUTPUT_NAME\""
wenzelm@49072
    77
    ;;
wenzelm@49072
    78
  *)
wenzelm@49072
    79
    ;;
wenzelm@49072
    80
esac
wenzelm@5570
    81
wenzelm@49072
    82
[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.eps" >&2
wenzelm@53774
    83
perl -p -e "s,<any>,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps"
wenzelm@48936
    84
wenzelm@49072
    85
[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.pdf" >&2
wenzelm@49072
    86
"$ISABELLE_EPSTOPDF" "${OUTPUT_NAME}.eps"
wenzelm@49072
    87