#!/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
[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" browser || exit $?; }
classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
if [ -n "$GRAPHFILE" ]; then
PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
if [ -n "$CLEAN" ]; then
mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
else
cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $FILE"
fi
PDF=""
case "$OUTFILE" in
*.pdf)
OUTFILE="${OUTFILE%%.pdf}.eps"
PDF=true
;;
esac
if [ -z "$OUTFILE" ]; then
"$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")"
else
"$ISABELLE_TOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")"
fi
RC="$?"
if [ -n "$PDF" ]; then
"$ISABELLE_EPSTOPDF" "$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_TOOL" java GraphBrowser.GraphBrowser
else
RC=0
fi
exit "$RC"