equal
deleted
inserted
replaced
63 |
63 |
64 classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar" |
64 classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar" |
65 |
65 |
66 if [ -z "$GRAPHFILE" ]; then |
66 if [ -z "$GRAPHFILE" ]; then |
67 [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" |
67 [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" |
68 exec "$ISATOOL" java GraphBrowser.GraphBrowser |
68 exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser |
69 else |
69 else |
70 PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE") |
70 PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE") |
71 if [ -n "$CLEAN" ]; then |
71 if [ -n "$CLEAN" ]; then |
72 mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE" |
72 mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE" |
73 else |
73 else |
81 PDF=true |
81 PDF=true |
82 ;; |
82 ;; |
83 esac |
83 esac |
84 |
84 |
85 if [ -z "$OUTFILE" ]; then |
85 if [ -z "$OUTFILE" ]; then |
86 "$ISATOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")" |
86 "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")" |
87 else |
87 else |
88 "$ISATOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")" |
88 "$ISABELLE_TOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")" |
89 fi |
89 fi |
90 RC="$?" |
90 RC="$?" |
91 |
91 |
92 if [ -n "$PDF" ]; then |
92 if [ -n "$PDF" ]; then |
93 "$ISABELLE_EPSTOPDF" "$OUTFILE" || fail "Failed to produce pdf output" |
93 "$ISABELLE_EPSTOPDF" "$OUTFILE" || fail "Failed to produce pdf output" |