# HG changeset patch
# User wenzelm
# Date 1616864501 -3600
# Node ID 92db3e31fae3e3ffcbc3fed58e19d67feb2642b3
# Parent  0e880b793db1d2a134575d738477673cfd77e708
clarified output;
more options;

diff -r 0e880b793db1 -r 92db3e31fae3 NEWS
--- a/NEWS	Sat Mar 27 17:13:15 2021 +0100
+++ b/NEWS	Sat Mar 27 18:01:41 2021 +0100
@@ -144,7 +144,7 @@
 *** System ***
 
 * Command-line tool "isabelle version" supports repository archives
-(without full .hg directory).
+(without full .hg directory). More options.
 
 
 
diff -r 0e880b793db1 -r 92db3e31fae3 lib/Tools/version
--- a/lib/Tools/version	Sat Mar 27 17:13:15 2021 +0100
+++ b/lib/Tools/version	Sat Mar 27 18:01:41 2021 +0100
@@ -15,6 +15,7 @@
   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
@@ -33,13 +34,17 @@
 # options
 
 SHORT_ID=""
+TAGS=""
 
-while getopts "i" OPT
+while getopts "it" OPT
 do
   case "$OPT" in
     i)
       SHORT_ID=true
       ;;
+    t)
+      TAGS=true
+      ;;
     \?)
       usage
       ;;
@@ -56,16 +61,33 @@
 
 ## main
 
-if [ -n "$SHORT_ID" ]; then
-  if [ -n "$ISABELLE_ID" ]; then
-    echo "$ISABELLE_ID"
-  elif [ -d "$ISABELLE_HOME/.hg" ]; then
-    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || echo undefined
-  elif [ -f "$ISABELLE_HOME/.hg_archival.txt" ]; then
-    fgrep node: < "$ISABELLE_HOME/.hg_archival.txt" | cut -d " " -f2 | head -c12
-  else
-    echo undefined
-  fi
-else
+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
diff -r 0e880b793db1 -r 92db3e31fae3 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Sat Mar 27 17:13:15 2021 +0100
+++ b/src/Doc/System/Misc.thy	Sat Mar 27 18:01:41 2021 +0100
@@ -367,6 +367,7 @@
 
   Options are:
     -i           short identification (derived from Mercurial id)
+    -t           symbolic tags (derived from Mercurial id)
 
   Display Isabelle version information.\<close>}
 
@@ -374,9 +375,13 @@
   The default is to output the full version string of the Isabelle
   distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2021: February 2021\<close>.
 
-  The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial
-  id of the @{setting ISABELLE_HOME} directory. This requires either a
-  repository clone or a repository archive (e.g. download of
+  \<^medskip>
+  Option \<^verbatim>\<open>-i\<close> produces a short identification derived from the Mercurial id
+  of the @{setting ISABELLE_HOME} directory; option \<^verbatim>\<open>-t\<close> prints version tags
+  (if available).
+
+  These options require either a repository clone or a repository archive
+  (e.g. download of
   \<^url>\<open>https://isabelle.sketis.net/repos/isabelle/archive/tip.tar.gz\<close>).
 \<close>