equal
deleted
inserted
replaced
59 [ "$#" -ne 0 ] && usage |
59 [ "$#" -ne 0 ] && usage |
60 |
60 |
61 |
61 |
62 ## main |
62 ## main |
63 |
63 |
64 export CLASSPATH="$ISABELLE_HOME/lib/browser/GraphBrowser.jar" |
64 export CLASSPATH="$(javapath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar")" |
|
65 |
65 if [ -z "$GRAPHFILE" ]; then |
66 if [ -z "$GRAPHFILE" ]; then |
66 cd "$ISABELLE_BROWSER_INFO" |
67 cd "$ISABELLE_BROWSER_INFO" |
67 exec java GraphBrowser.GraphBrowser |
68 exec java GraphBrowser.GraphBrowser |
68 else |
69 else |
69 PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE") |
70 PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE") |
80 PDF=true |
81 PDF=true |
81 ;; |
82 ;; |
82 esac |
83 esac |
83 |
84 |
84 if [ -z "$OUTFILE" ]; then |
85 if [ -z "$OUTFILE" ]; then |
85 java GraphBrowser.GraphBrowser "$PRIVATE_FILE" |
86 java GraphBrowser.GraphBrowser "$(javapath "$PRIVATE_FILE")" |
86 else |
87 else |
87 java GraphBrowser.Console "$PRIVATE_FILE" "$OUTFILE" |
88 java GraphBrowser.Console "$(javapath "$PRIVATE_FILE")" "$(javapath "$OUTFILE")" |
88 fi |
89 fi |
89 RC="$?" |
90 RC="$?" |
90 |
91 |
91 if [ -n "$PDF" ]; then |
92 if [ -n "$PDF" ]; then |
92 "$ISABELLE_EPSTOPDF" "$OUTFILE" || fail "Failed to produce pdf output" |
93 "$ISABELLE_EPSTOPDF" "$OUTFILE" || fail "Failed to produce pdf output" |