lib/Tools/print
author hoelzl
Mon, 06 Dec 2010 19:54:48 +0100
changeset 41024 ba961a606c67
parent 29143 72c960b2b83e
permissions -rwxr-xr-x
move coercions to appropriate places
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14931
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     2
#
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     4
#
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: print document
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     6
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     7
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     8
PRG="$(basename "$0")"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     9
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    10
function usage()
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    11
{
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    12
  echo
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 15010
diff changeset
    13
  echo "Usage: isabelle $PRG [OPTIONS] FILE"
14931
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    14
  echo
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    15
  echo "  Options are:"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    16
  echo "    -c           cleanup -- remove FILE after use"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    17
  echo
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    18
  echo "  Print document FILE."
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    19
  echo
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    20
  exit 1
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    21
}
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    22
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    23
function fail()
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    24
{
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    25
  echo "$1" >&2
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    26
  exit 2
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    27
}
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    28
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    29
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    30
## process command line
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    31
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    32
# options
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    33
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    34
CLEAN=""
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    35
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    36
while getopts "c" OPT
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    37
do
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    38
  case "$OPT" in
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    39
    c)
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    40
      CLEAN=true
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    41
      ;;
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    42
    \?)
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    43
      usage
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    44
      ;;
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    45
  esac
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    46
done
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    47
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    48
shift $(($OPTIND - 1))
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    49
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    50
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    51
# args
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    52
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    53
[ "$#" -ne 1 ] && usage
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    54
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    55
FILE="$1"; shift
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    56
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    57
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    58
## main
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    59
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    60
[ -f "$FILE" ] || fail "Bad file: $FILE"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    61
$PRINT_COMMAND "$FILE"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    62
[ -n "$CLEAN" ] && rm -f "$FILE"