lib/Tools/version

more robust and uniform ISABELLE_TAGS;

#!/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

HG_ARCHIVAL="$ISABELLE_HOME/.hg_archival.txt"

export LANG=C
export HGPLAIN=

if [ -n "$SHORT_ID" ]; then
  if [ -f "$ISABELLE_HOME/etc/ISABELLE_ID" ]; then
    RESULT="$(cat "$ISABELLE_HOME/etc/ISABELLE_ID")"
    RC="$?"
  elif [ -d "$ISABELLE_HOME/.hg" ]; then
    RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null)
    RC="$?"
  elif [ -f "$HG_ARCHIVAL" ]; then
    RESULT="$(grep "^node:" < "$HG_ARCHIVAL" | cut -d " " -f2 | head -c12)"
    RC="$?"
  else
    RESULT=""
    RC="0"
  fi
  if [ "$RC" -ne 0 ]; then
    exit "$RC"
  elif [ -n "$RESULT" ]; then
    echo "$RESULT"
  fi
fi

if [ -n "$TAGS" ]; then
  if [ -f "$ISABELLE_HOME/etc/ISABELLE_TAGS" ]; then
    RESULT="$(cat "$ISABELLE_HOME/etc/ISABELLE_TAGS")"
    RC="$?"
  elif [ -d "$ISABELLE_HOME/.hg" ]; then
    RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" id -t 2>/dev/null)
    RC="$?"
  elif [ -f "$HG_ARCHIVAL" ]; then
    RESULT="$(grep "^tag:" < "$HG_ARCHIVAL" | cut -d " " -f2)"
    RC="$?"
  else
    RESULT=""
    RC="0"
  fi
  if [ "$RC" -ne 0 ]; then
    exit "$RC"
  elif [ -n "$RESULT" -a "$RESULT" != "tip" ]; then
    echo "$RESULT"
  fi
fi