| author | wenzelm |
| Sun, 19 Jan 2025 21:02:03 +0100 | |
| changeset 81928 | d6366c0c9d5c |
| parent 74038 | b4f57bfe82e7 |
| 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 |
||
|
74038
b4f57bfe82e7
more robust "isabelle build_scala" as separate tool;
wenzelm
parents:
74017
diff
changeset
|
68 |
isabelle scala_build || exit $? |
| 25650 | 69 |
|
| 35587 | 70 |
if [ -n "$GRAPHFILE" ]; then |
|
58639
1df53737c59b
prefer Unix standard-conformant $TMPDIR over hard-wired /tmp;
wenzelm
parents:
57082
diff
changeset
|
71 |
PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE")
|
| 20569 | 72 |
if [ -n "$CLEAN" ]; then |
| 49562 | 73 |
mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE" |
| 20569 | 74 |
else |
| 49562 | 75 |
cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPHFILE" |
| 20569 | 76 |
fi |
77 |
||
| 11843 | 78 |
PDF="" |
| 11801 | 79 |
case "$OUTFILE" in |
80 |
*.pdf) |
|
| 11843 | 81 |
OUTFILE="${OUTFILE%%.pdf}.eps"
|
| 11801 | 82 |
PDF=true |
83 |
;; |
|
84 |
esac |
|
85 |
||
| 11843 | 86 |
if [ -z "$OUTFILE" ]; then |
| 74015 | 87 |
isabelle java isabelle.graphbrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")" |
| 11813 | 88 |
else |
| 74015 | 89 |
isabelle java isabelle.graphbrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")" |
| 11813 | 90 |
fi |
| 11843 | 91 |
RC="$?" |
| 11801 | 92 |
|
93 |
if [ -n "$PDF" ]; then |
|
| 57082 | 94 |
( |
95 |
cd "$(dirname "$OUTFILE")" |
|
96 |
"$ISABELLE_EPSTOPDF" "$(basename "$OUTFILE")" || fail "Failed to produce pdf output" |
|
97 |
) |
|
| 11801 | 98 |
fi |
99 |
||
| 20569 | 100 |
rm -f "$PRIVATE_FILE" |
| 35587 | 101 |
elif [ -z "$ADMIN_BUILD" ]; then |
102 |
[ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" |
|
| 74015 | 103 |
exec isabelle java isabelle.graphbrowser.GraphBrowser |
| 35587 | 104 |
else |
105 |
RC=0 |
|
| 9794 | 106 |
fi |
| 11843 | 107 |
|
108 |
exit "$RC" |