author | nipkow |
Fri, 08 Aug 2014 08:26:32 +0200 | |
changeset 57817 | dfebc374bd89 |
parent 57082 | 2c1c8b38e3f0 |
child 58639 | 1df53737c59b |
permissions | -rwxr-xr-x |
10555 | 1 |
#!/usr/bin/env bash |
3640 | 2 |
# |
9788 | 3 |
# Author: Markus Wenzel, TU Muenchen |
3640 | 4 |
# |
7766 | 5 |
# DESCRIPTION: Isabelle graph browser |
3640 | 6 |
|
7 |
||
10511 | 8 |
PRG="$(basename "$0")" |
3640 | 9 |
|
10 |
function usage() |
|
11 |
{ |
|
12 |
echo |
|
28650 | 13 |
echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]" |
3640 | 14 |
echo |
7766 | 15 |
echo " Options are:" |
35587 | 16 |
echo " -b Admin/build only" |
20569 | 17 |
echo " -c cleanup -- remove GRAPHFILE after use" |
11801 | 18 |
echo " -o FILE output to FILE (ps, eps, pdf)" |
7766 | 19 |
echo |
3640 | 20 |
exit 1 |
21 |
} |
|
22 |
||
11801 | 23 |
function fail() |
24 |
{ |
|
25 |
echo "$1" >&2 |
|
26 |
exit 2 |
|
27 |
} |
|
28 |
||
29 |
||
7766 | 30 |
## process command line |
31 |
||
32 |
# options |
|
33 |
||
35587 | 34 |
ADMIN_BUILD="" |
20569 | 35 |
CLEAN="" |
11801 | 36 |
OUTFILE="" |
7766 | 37 |
|
35587 | 38 |
while getopts "bco:" OPT |
7766 | 39 |
do |
40 |
case "$OPT" in |
|
35587 | 41 |
b) |
42 |
ADMIN_BUILD=true |
|
43 |
;; |
|
20569 | 44 |
c) |
45 |
CLEAN=true |
|
7766 | 46 |
;; |
11801 | 47 |
o) |
48 |
OUTFILE="$OPTARG" |
|
49 |
;; |
|
7766 | 50 |
\?) |
51 |
usage |
|
52 |
;; |
|
53 |
esac |
|
54 |
done |
|
55 |
||
56 |
shift $(($OPTIND - 1)) |
|
57 |
||
58 |
||
59 |
# args |
|
60 |
||
61 |
GRAPHFILE="" |
|
9788 | 62 |
[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; } |
63 |
[ "$#" -ne 0 ] && usage |
|
7766 | 64 |
|
3640 | 65 |
|
66 |
## main |
|
67 |
||
52443 | 68 |
isabelle_admin_build browser || exit $? |
34283
7911e83d06c0
simplified build/bootstrap of graph browser -- avoid make;
wenzelm
parents:
29143
diff
changeset
|
69 |
|
27907 | 70 |
classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar" |
25650 | 71 |
|
35587 | 72 |
if [ -n "$GRAPHFILE" ]; then |
20569 | 73 |
PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE") |
74 |
if [ -n "$CLEAN" ]; then |
|
49562 | 75 |
mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE" |
20569 | 76 |
else |
49562 | 77 |
cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPHFILE" |
20569 | 78 |
fi |
79 |
||
11843 | 80 |
PDF="" |
11801 | 81 |
case "$OUTFILE" in |
82 |
*.pdf) |
|
11843 | 83 |
OUTFILE="${OUTFILE%%.pdf}.eps" |
11801 | 84 |
PDF=true |
85 |
;; |
|
86 |
esac |
|
87 |
||
11843 | 88 |
if [ -z "$OUTFILE" ]; then |
28500 | 89 |
"$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")" |
11813 | 90 |
else |
28500 | 91 |
"$ISABELLE_TOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")" |
11813 | 92 |
fi |
11843 | 93 |
RC="$?" |
11801 | 94 |
|
95 |
if [ -n "$PDF" ]; then |
|
57082 | 96 |
( |
97 |
cd "$(dirname "$OUTFILE")" |
|
98 |
"$ISABELLE_EPSTOPDF" "$(basename "$OUTFILE")" || fail "Failed to produce pdf output" |
|
99 |
) |
|
11801 | 100 |
fi |
101 |
||
20569 | 102 |
rm -f "$PRIVATE_FILE" |
35587 | 103 |
elif [ -z "$ADMIN_BUILD" ]; then |
104 |
[ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" |
|
105 |
exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser |
|
106 |
else |
|
107 |
RC=0 |
|
9794 | 108 |
fi |
11843 | 109 |
|
110 |
exit "$RC" |