more robust and uniform ISABELLE_TAGS;

--- a/lib/Tools/version	Wed Mar 31 18:12:46 2021 +0200
+++ b/lib/Tools/version	Wed Mar 31 21:44:29 2021 +0200
@@ -72,24 +72,38 @@
 
 if [ -n "$SHORT_ID" ]; then
   if [ -f "$ISABELLE_HOME/etc/ISABELLE_ID" ]; then
-    ID="$(cat "$ISABELLE_HOME/etc/ISABELLE_ID")"
-    echo "$ID"
+    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)"
-    [ -n "$RESULT" ] && echo "$RESULT"
-  elif [ -d "$ISABELLE_HOME/.hg" ]; then
-    "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || exit "$?"
+    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
-  RESULT=""
-  if [ -d "$ISABELLE_HOME/.hg" ]; 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"

--- a/src/Pure/Admin/build_release.scala	Wed Mar 31 18:12:46 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed Mar 31 21:44:29 2021 +0200
@@ -25,11 +25,13 @@
     val dist_name: String,
     val dist_dir: Path,
     val dist_version: String,
-    val ident: String)
+    val ident: String,
+    val tags: String)
   {
     val isabelle: Path = Path.explode(dist_name)
     val isabelle_dir: Path = dist_dir + isabelle
     val isabelle_id: Path = isabelle_dir + Path.explode("etc/ISABELLE_ID")
+    val isabelle_tags: Path = isabelle_dir + Path.explode("etc/ISABELLE_TAGS")
     val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
     val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
 
@@ -398,6 +400,7 @@
       val ident =
         try { hg.id(version) }
         catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
+      val tags = hg.tags(rev = ident)
 
       val dist_version =
         proper_release_name match {
@@ -405,7 +408,7 @@
           case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
         }
 
-      new Release(progress, date, dist_name, dist_dir, dist_version, ident)
+      new Release(progress, date, dist_name, dist_dir, dist_version, ident, tags)
     }
 
 
@@ -450,6 +453,7 @@
       progress.echo_warning("Preparing distribution " + quote(release.dist_name))
 
       File.write(release.isabelle_id, release.ident)
+      File.write(release.isabelle_tags, release.tags)
 
       patch_release(release)
 

--- a/src/Pure/General/mercurial.scala	Wed Mar 31 18:12:46 2021 +0200
+++ b/src/Pure/General/mercurial.scala	Wed Mar 31 21:44:29 2021 +0200
@@ -32,10 +32,12 @@
   /* repository archives */
 
   private val Archive_Node = """^node: (\S{12}).*$""".r
+  private val Archive_Tag = """^tag: (\S+).*$""".r
 
   sealed case class Archive_Info(lines: List[String])
   {
     def id: Option[String] = lines.collectFirst({ case Archive_Node(a) => a })
+    def tags: List[String] = for (Archive_Tag(tag) <- lines if tag != "tip") yield tag
   }
 
   def archive_info(root: Path): Option[Archive_Info] =
@@ -44,7 +46,11 @@
     if (path.is_file) Some(Archive_Info(Library.trim_split_lines(File.read(path)))) else None
   }
 
-  def archive_id(root: Path): Option[String] = archive_info(root).flatMap(_.id)
+  def archive_id(root: Path): Option[String] =
+    archive_info(root).flatMap(_.id)
+
+  def archive_tags(root: Path): Option[String] =
+    archive_info(root).map(info => info.tags.mkString(" "))
 
 
   /* repository access */
@@ -126,6 +132,8 @@
 
     def id(rev: String = "tip"): String = identify(rev, options = "-i")
 
+    def tags(rev: String = "tip"): String = identify(rev, options = "-t")
+
     def paths(args: String = "", options: String = ""): List[String] =
       hg.command("paths", args = args, options = options).check.out_lines
 

--- a/src/Pure/System/isabelle_system.scala	Wed Mar 31 18:12:46 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Mar 31 21:44:29 2021 +0200
@@ -187,7 +187,7 @@
   }
 
 
-  /* Isabelle distribution identifier */
+  /* Isabelle distribution identification */
 
   def isabelle_id(root: Path = Path.explode("~~")): Option[String] =
     getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) orElse {
@@ -195,6 +195,14 @@
       else None
     }
 
+  def isabelle_tags(root: Path = Path.explode("~~")): String =
+    getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse {
+      if (Mercurial.is_repository(root)) {
+        val hg = Mercurial.repository(root)
+        hg.tags(rev = hg.parent())
+      }
+      else ""
+    }
 
 
   /** file-system operations **/