equal
deleted
inserted
replaced
65 export CLASSPATH="$ISABELLE_HOME/lib/browser" |
65 export CLASSPATH="$ISABELLE_HOME/lib/browser" |
66 if [ -z "$GRAPHFILE" ]; then |
66 if [ -z "$GRAPHFILE" ]; then |
67 cd "$ISABELLE_BROWSER_INFO" |
67 cd "$ISABELLE_BROWSER_INFO" |
68 exec java GraphBrowser.GraphBrowser |
68 exec java GraphBrowser.GraphBrowser |
69 else |
69 else |
|
70 PDF="" |
70 case "$OUTFILE" in |
71 case "$OUTFILE" in |
71 *.pdf) |
72 *.pdf) |
72 TMPOUTFILE="${OUTFILE%.pdf}.eps" |
73 OUTFILE="${OUTFILE%%.pdf}.eps" |
73 PDF=true |
74 PDF=true |
74 ;; |
|
75 *) |
|
76 TMPOUTFILE="$OUTFILE" |
|
77 PDF="" |
|
78 ;; |
75 ;; |
79 esac |
76 esac |
80 |
77 |
81 if [ -z "$TMPOUTFILE" ]; then |
78 if [ -z "$OUTFILE" ]; then |
82 java GraphBrowser.GraphBrowser "$GRAPHFILE" |
79 java GraphBrowser.GraphBrowser "$GRAPHFILE" |
83 else |
80 else |
84 java GraphBrowser.GraphBrowser "$GRAPHFILE" "$TMPOUTFILE" |
81 unset DISPLAY #paranoia setting |
|
82 java GraphBrowser.GraphBrowser "$GRAPHFILE" "$OUTFILE" |
85 fi |
83 fi |
|
84 RC="$?" |
86 |
85 |
87 if [ -n "$PDF" ]; then |
86 if [ -n "$PDF" ]; then |
88 "$ISABELLE_EPSTOPDF" "$TMPOUTFILE" || fail "Failed to produce pdf output" |
87 "$ISABELLE_EPSTOPDF" "$OUTFILE" || fail "Failed to produce pdf output" |
89 rm -f "$TMPOUTFILE" |
|
90 fi |
88 fi |
91 |
89 |
92 [ -n "$DELETE" ] && rm -f "$GRAPHFILE" |
90 [ -n "$DELETE" ] && rm -f "$GRAPHFILE" |
93 fi |
91 fi |
|
92 |
|
93 exit "$RC" |