# HG changeset patch
# User wenzelm
# Date 1294772134 -3600
# Node ID 2fe62d6026814c6f601372401f0a3c2f03be3609
# Parent  75c6c40699387675f71286ce9a078921b6cec4e2
isabelle version -i;

diff -r 75c6c4069938 -r 2fe62d602681 Admin/makedist
--- a/Admin/makedist	Tue Jan 11 18:23:29 2011 +0100
+++ b/Admin/makedist	Tue Jan 11 19:55:34 2011 +0100
@@ -169,6 +169,7 @@
 fi
 
 perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
+perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
 perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
diff -r 75c6c4069938 -r 2fe62d602681 doc-src/System/Thy/Misc.thy
--- a/doc-src/System/Thy/Misc.thy	Tue Jan 11 18:23:29 2011 +0100
+++ b/doc-src/System/Thy/Misc.thy	Tue Jan 11 19:55:34 2011 +0100
@@ -281,9 +281,21 @@
 section {* Output the version identifier of the Isabelle distribution *}
 
 text {*
-  The @{tool_def version} utility outputs the full version string of
-  the Isabelle distribution being used, e.g.\ ``@{verbatim
-  "Isabelle2008: June 2008"}.  There are no options nor arguments.
+  The @{tool_def version} utility displays Isabelle version information:
+\begin{ttbox}
+Usage: isabelle version [OPTIONS]
+
+  Options are:
+    -i           short identification (derived from Mercurial id)
+
+  Display Isabelle version information.
+\end{ttbox}
+
+  \medskip The default is to output the full version string of the
+  Isabelle distribution, e.g.\ ``@{verbatim "Isabelle2008: June 2008"}.
+
+  The @{verbatim "-i"} option produces a short identification derived
+  from the Mercurial id of the @{setting ISABELLE_HOME} directory.
 *}
 
 
diff -r 75c6c4069938 -r 2fe62d602681 doc-src/System/Thy/document/Misc.tex
--- a/doc-src/System/Thy/document/Misc.tex	Tue Jan 11 18:23:29 2011 +0100
+++ b/doc-src/System/Thy/document/Misc.tex	Tue Jan 11 19:55:34 2011 +0100
@@ -320,8 +320,21 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The \indexdef{}{tool}{version}\hypertarget{tool.version}{\hyperlink{tool.version}{\mbox{\isa{\isatt{version}}}}} utility outputs the full version string of
-  the Isabelle distribution being used, e.g.\ ``\verb|Isabelle2008: June 2008|.  There are no options nor arguments.%
+The \indexdef{}{tool}{version}\hypertarget{tool.version}{\hyperlink{tool.version}{\mbox{\isa{\isatt{version}}}}} utility displays Isabelle version information:
+\begin{ttbox}
+Usage: isabelle version [OPTIONS]
+
+  Options are:
+    -i           short identification (derived from Mercurial id)
+
+  Display Isabelle version information.
+\end{ttbox}
+
+  \medskip The default is to output the full version string of the
+  Isabelle distribution, e.g.\ ``\verb|Isabelle2008: June 2008|.
+
+  The \verb|-i| option produces a short identification derived
+  from the Mercurial id of the \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} directory.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 75c6c4069938 -r 2fe62d602681 lib/Tools/version
--- a/lib/Tools/version	Tue Jan 11 18:23:29 2011 +0100
+++ b/lib/Tools/version	Tue Jan 11 19:55:34 2011 +0100
@@ -1,7 +1,67 @@
 #!/usr/bin/env bash
 #
 # Author: Stefan Berghofer, TU Muenchen
+# Author: Makarius
 #
 # DESCRIPTION: display Isabelle version
 
-echo 'unidentified repository version'    # filled in automatically!
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS]"
+  echo
+  echo "  Options are:"
+  echo "    -i           short identification (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=""
+
+while getopts "i" OPT
+do
+  case "$OPT" in
+    i)
+      SHORT_ID=true
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ "$#" -ne 0 ] && usage
+
+
+## main
+
+if [ -n "$SHORT_ID" ]; then
+  if [ -n "$ISABELLE_ID" ]; then
+    echo "$ISABELLE_ID"
+  else
+    ${HG:-hg} id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
+  fi
+else
+  echo 'unidentified repository version'    # filled in automatically!
+fi
diff -r 75c6c4069938 -r 2fe62d602681 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Tue Jan 11 18:23:29 2011 +0100
+++ b/lib/scripts/getsettings	Tue Jan 11 19:55:34 2011 +0100
@@ -31,9 +31,10 @@
 . "$ISABELLE_HOME/lib/scripts/isabelle-platform"
 
 #Isabelle distribution identifier -- filled in automatically!
+ISABELLE_ID=""
 ISABELLE_IDENTIFIER=""
 
-#users tend to put strange things in here ...
+#sometimes users put strange things in here ...
 unset ENV
 unset BASH_ENV