equal
deleted
inserted
replaced
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]" |
13 echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]" |
14 echo |
14 echo |
15 echo " Options are:" |
15 echo " Options are:" |
|
16 echo " -b Admin/build only" |
16 echo " -c cleanup -- remove GRAPHFILE after use" |
17 echo " -c cleanup -- remove GRAPHFILE after use" |
17 echo " -o FILE output to FILE (ps, eps, pdf)" |
18 echo " -o FILE output to FILE (ps, eps, pdf)" |
18 echo |
19 echo |
19 exit 1 |
20 exit 1 |
20 } |
21 } |
28 |
29 |
29 ## process command line |
30 ## process command line |
30 |
31 |
31 # options |
32 # options |
32 |
33 |
|
34 ADMIN_BUILD="" |
33 CLEAN="" |
35 CLEAN="" |
34 OUTFILE="" |
36 OUTFILE="" |
35 |
37 |
36 while getopts "co:" OPT |
38 while getopts "bco:" OPT |
37 do |
39 do |
38 case "$OPT" in |
40 case "$OPT" in |
|
41 b) |
|
42 ADMIN_BUILD=true |
|
43 ;; |
39 c) |
44 c) |
40 CLEAN=true |
45 CLEAN=true |
41 ;; |
46 ;; |
42 o) |
47 o) |
43 OUTFILE="$OPTARG" |
48 OUTFILE="$OPTARG" |
62 |
67 |
63 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" browser || exit $?; } |
68 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" browser || exit $?; } |
64 |
69 |
65 classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar" |
70 classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar" |
66 |
71 |
67 if [ -z "$GRAPHFILE" ]; then |
72 if [ -n "$GRAPHFILE" ]; then |
68 [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" |
|
69 exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser |
|
70 else |
|
71 PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE") |
73 PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE") |
72 if [ -n "$CLEAN" ]; then |
74 if [ -n "$CLEAN" ]; then |
73 mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE" |
75 mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE" |
74 else |
76 else |
75 cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $FILE" |
77 cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $FILE" |
93 if [ -n "$PDF" ]; then |
95 if [ -n "$PDF" ]; then |
94 "$ISABELLE_EPSTOPDF" "$OUTFILE" || fail "Failed to produce pdf output" |
96 "$ISABELLE_EPSTOPDF" "$OUTFILE" || fail "Failed to produce pdf output" |
95 fi |
97 fi |
96 |
98 |
97 rm -f "$PRIVATE_FILE" |
99 rm -f "$PRIVATE_FILE" |
|
100 elif [ -z "$ADMIN_BUILD" ]; then |
|
101 [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" |
|
102 exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser |
|
103 else |
|
104 RC=0 |
98 fi |
105 fi |
99 |
106 |
100 exit "$RC" |
107 exit "$RC" |