#!/usr/bin/env bash
#
# Author: Stefan Berghofer, TU Muenchen
# Author: Makarius
#
# DESCRIPTION: display Isabelle version
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS]"
echo
echo " Options are:"
echo " -i short identification (derived from Mercurial id)"
echo " -t symbolic tags (derived from Mercurial id)"
echo
echo " Display Isabelle version information."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
# options
SHORT_ID=""
TAGS=""
while getopts "it" OPT
do
case "$OPT" in
i)
SHORT_ID=true
;;
t)
TAGS=true
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
# args
[ "$#" -ne 0 ] && usage
## main
if [ -z "$SHORT_ID" -a -z "$TAGS" ]; then
echo 'repository version' # filled in automatically!
fi
if [ -n "$SHORT_ID" ]; then
if [ -d "$ISABELLE_HOME/.hg" ]; then
"${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || exit "$?"
elif [ -f "$ISABELLE_HOME/.hg_archival.txt" ]; then
RESULT="$(fgrep node: < "$ISABELLE_HOME/.hg_archival.txt" | cut -d " " -f2 | head -c12)"
[ -n "$RESULT" ] && echo "$RESULT"
elif [ -n "$ISABELLE_ID" ]; then
echo "$ISABELLE_ID"
fi
fi
if [ -n "$TAGS" ]; then
RESULT=""
if [ -d "$ISABELLE_HOME/.hg" ]; then
RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" id -t 2>/dev/null)
RC="$?"
elif [ -f "$ISABELLE_HOME/.hg_archival.txt" ]; then
RESULT="$(fgrep tag: < "$ISABELLE_HOME/.hg_archival.txt" | cut -d " " -f2)"
RC="$?"
fi
if [ "$RC" -ne 0 ]; then
exit "$RC"
elif [ -n "$RESULT" -a "$RESULT" != "tip" ]; then
echo "$RESULT"
fi
fi