#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: Isabelle graph browser
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]"
echo
echo " Options are:"
echo " -b Admin/build only"
echo " -c cleanup -- remove GRAPHFILE after use"
echo " -o FILE output to FILE (ps, eps, pdf)"
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
# options
ADMIN_BUILD=""
CLEAN=""
OUTFILE=""
while getopts "bco:" OPT
do
case "$OPT" in
b)
ADMIN_BUILD=true
;;
c)
CLEAN=true
;;
o)
OUTFILE="$OPTARG"
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
# args
GRAPHFILE=""
[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
[ "$#" -ne 0 ] && usage
## main
isabelle_admin_build browser || exit $?
classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
if [ -n "$GRAPHFILE" ]; then
PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE")
if [ -n "$CLEAN" ]; then
mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE"
else
cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPHFILE"
fi
PDF=""
case "$OUTFILE" in
*.pdf)
OUTFILE="${OUTFILE%%.pdf}.eps"
PDF=true
;;
esac
if [ -z "$OUTFILE" ]; then
isabelle java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
else
isabelle java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
fi
RC="$?"
if [ -n "$PDF" ]; then
(
cd "$(dirname "$OUTFILE")"
"$ISABELLE_EPSTOPDF" "$(basename "$OUTFILE")" || fail "Failed to produce pdf output"
)
fi
rm -f "$PRIVATE_FILE"
elif [ -z "$ADMIN_BUILD" ]; then
[ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
exec isabelle java GraphBrowser.GraphBrowser
else
RC=0
fi
exit "$RC"