lib/Tools/version
author wenzelm
Wed, 06 Apr 2011 21:55:41 +0200
changeset 42262 4821a2a91548
parent 41511 2fe62d602681
child 48837 d1d806a42c91
permissions -rwxr-xr-x
moved type syntax translations to syn_trans.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13804
d643300e4fc0 New tool for displaying version information.
berghofe
parents:
diff changeset
     1
#!/usr/bin/env bash
d643300e4fc0 New tool for displaying version information.
berghofe
parents:
diff changeset
     2
#
d643300e4fc0 New tool for displaying version information.
berghofe
parents:
diff changeset
     3
# Author: Stefan Berghofer, TU Muenchen
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
     4
# Author: Makarius
13804
d643300e4fc0 New tool for displaying version information.
berghofe
parents:
diff changeset
     5
#
d643300e4fc0 New tool for displaying version information.
berghofe
parents:
diff changeset
     6
# DESCRIPTION: display Isabelle version
d643300e4fc0 New tool for displaying version information.
berghofe
parents:
diff changeset
     7
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
     8
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
     9
PRG="$(basename "$0")"
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    10
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    11
function usage()
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    12
{
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    13
  echo
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    14
  echo "Usage: isabelle $PRG [OPTIONS]"
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    15
  echo
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    16
  echo "  Options are:"
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    17
  echo "    -i           short identification (derived from Mercurial id)"
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    18
  echo
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    19
  echo "  Display Isabelle version information."
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    20
  echo
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    21
  exit 1
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    22
}
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    23
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    24
function fail()
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    25
{
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    26
  echo "$1" >&2
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    27
  exit 2
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    28
}
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    29
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    30
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    31
## process command line
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    32
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    33
# options
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    34
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    35
SHORT_ID=""
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    36
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    37
while getopts "i" OPT
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    38
do
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    39
  case "$OPT" in
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    40
    i)
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    41
      SHORT_ID=true
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    42
      ;;
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    43
    \?)
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    44
      usage
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    45
      ;;
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    46
  esac
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    47
done
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    48
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    49
shift $(($OPTIND - 1))
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    50
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    51
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    52
# args
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    53
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    54
[ "$#" -ne 0 ] && usage
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    55
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    56
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    57
## main
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    58
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    59
if [ -n "$SHORT_ID" ]; then
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    60
  if [ -n "$ISABELLE_ID" ]; then
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    61
    echo "$ISABELLE_ID"
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    62
  else
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    63
    ${HG:-hg} id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    64
  fi
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    65
else
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    66
  echo 'unidentified repository version'    # filled in automatically!
2fe62d602681 isabelle version -i;
wenzelm
parents: 32361
diff changeset
    67
fi