lib/Tools/logo
author wenzelm
Wed Nov 07 21:42:16 2018 +0100 (9 months ago)
changeset 69255 800b1ce96fce
parent 53774 729a43c36ccb
permissions -rwxr-xr-x
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # DESCRIPTION: create an instance of the Isabelle logo
     6 
     7 
     8 PRG="$(basename "$0")"
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: isabelle $PRG [OPTIONS] [XYZ]"
    14   echo
    15   echo "  Create instance XYZ of the Isabelle logo (as EPS and PDF)."
    16   echo
    17   echo "  Options are:"
    18   echo "    -n NAME      alternative output base name (default \"isabelle_xyx\")"
    19   echo "    -q           quiet mode"
    20   echo
    21   exit 1
    22 }
    23 
    24 function fail()
    25 {
    26   echo "$1" >&2
    27   exit 2
    28 }
    29 
    30 
    31 ## process command line
    32 
    33 # options
    34 
    35 OUTPUT_NAME=""
    36 QUIET=""
    37 
    38 while getopts "n:q" OPT
    39 do
    40   case "$OPT" in
    41     n)
    42       OUTPUT_NAME="$OPTARG"
    43       ;;
    44     q)
    45       QUIET=true
    46       ;;
    47     \?)
    48       usage
    49       ;;
    50   esac
    51 done
    52 
    53 shift $(($OPTIND - 1))
    54 
    55 
    56 # args
    57 
    58 TEXT=""
    59 [ "$#" -ge 1 ] && { TEXT="$1"; shift; }
    60 
    61 [ "$#" -ne 0 ] && usage
    62 
    63 
    64 ## main
    65 
    66 case "$OUTPUT_NAME" in
    67   "")
    68     OUTPUT_NAME=$(echo "$TEXT" | tr A-Z a-z)
    69     if [ -z "$OUTPUT_NAME" ]; then
    70       OUTPUT_NAME="isabelle"
    71     else
    72       OUTPUT_NAME="isabelle_${OUTPUT_NAME}"
    73     fi
    74     ;;
    75   */* | *.eps | *.pdf)
    76     fail "Bad output base name: \"$OUTPUT_NAME\""
    77     ;;
    78   *)
    79     ;;
    80 esac
    81 
    82 [ -z "$QUIET" ] && echo "${OUTPUT_NAME}.eps" >&2
    83 perl -p -e "s,<any>,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "${OUTPUT_NAME}.eps"
    84 
    85 [ -z "$QUIET" ] && echo "${OUTPUT_NAME}.pdf" >&2
    86 "$ISABELLE_EPSTOPDF" "${OUTPUT_NAME}.eps"
    87