equal
deleted
inserted
replaced
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" |
|