lib/Tools/logo
author wenzelm
Sat, 22 Mar 2014 18:19:57 +0100
changeset 56254 a2dd9200854d
parent 53774 729a43c36ccb
child 72316 3cc6aa405858
permissions -rwxr-xr-x
more antiquotations;
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
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    13
  echo "Usage: isabelle $PRG [OPTIONS] [XYZ]"
5570
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    14
  echo
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    15
  echo "  Create instance XYZ of the Isabelle logo (as EPS and PDF)."
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:"
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    18
  echo "    -n NAME      alternative output base name (default \"isabelle_xyx\")"
5570
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
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    35
OUTPUT_NAME=""
5570
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    36
QUIET=""
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    37
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    38
while getopts "n:q" OPT
5570
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    39
do
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    40
  case "$OPT" in
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    41
    n)
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    42
      OUTPUT_NAME="$OPTARG"
5570
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
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    58
TEXT=""
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    59
[ "$#" -ge 1 ] && { TEXT="$1"; shift; }
5557
d6ceb4275742 create an instance of the Isabelle logo;
wenzelm
parents:
diff changeset
    60
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    61
[ "$#" -ne 0 ] && 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
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    66
case "$OUTPUT_NAME" in
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    67
  "")
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    68
    OUTPUT_NAME=$(echo "$TEXT" | tr A-Z a-z)
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    69
    if [ -z "$OUTPUT_NAME" ]; then
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    70
      OUTPUT_NAME="isabelle"
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    71
    else
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    72
      OUTPUT_NAME="isabelle_${OUTPUT_NAME}"
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    73
    fi
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    74
    ;;
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    75
  */* | *.eps | *.pdf)
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    76
    fail "Bad output base name: \"$OUTPUT_NAME\""
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    77
    ;;
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    78
  *)
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    79
    ;;
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    80
esac
5570
ae1b56ef16b0 improved;
wenzelm
parents: 5557
diff changeset
    81
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    82
[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.eps" >&2
53774
729a43c36ccb proper text replacement (cf. 747835eb2782);
wenzelm
parents: 49072
diff changeset
    83
perl -p -e "s,<any>,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps"
48936
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 29143
diff changeset
    84
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    85
[ -z "$QUIET" ] && echo "${OUTPUT_NAME}.pdf" >&2
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    86
"$ISABELLE_EPSTOPDF" "${OUTPUT_NAME}.eps"
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48936
diff changeset
    87