lib/Tools/print
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 29143 72c960b2b83e
permissions -rwxr-xr-x
renamed structure Display_Goal to Goal_Display;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # DESCRIPTION: print document
     6 
     7 
     8 PRG="$(basename "$0")"
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: isabelle $PRG [OPTIONS] FILE"
    14   echo
    15   echo "  Options are:"
    16   echo "    -c           cleanup -- remove FILE after use"
    17   echo
    18   echo "  Print document FILE."
    19   echo
    20   exit 1
    21 }
    22 
    23 function fail()
    24 {
    25   echo "$1" >&2
    26   exit 2
    27 }
    28 
    29 
    30 ## process command line
    31 
    32 # options
    33 
    34 CLEAN=""
    35 
    36 while getopts "c" OPT
    37 do
    38   case "$OPT" in
    39     c)
    40       CLEAN=true
    41       ;;
    42     \?)
    43       usage
    44       ;;
    45   esac
    46 done
    47 
    48 shift $(($OPTIND - 1))
    49 
    50 
    51 # args
    52 
    53 [ "$#" -ne 1 ] && usage
    54 
    55 FILE="$1"; shift
    56 
    57 
    58 ## main
    59 
    60 [ -f "$FILE" ] || fail "Bad file: $FILE"
    61 $PRINT_COMMAND "$FILE"
    62 [ -n "$CLEAN" ] && rm -f "$FILE"