clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;

--- a/lib/Tools/version	Wed Mar 31 17:15:54 2021 +0200
+++ b/lib/Tools/version	Wed Mar 31 18:12:46 2021 +0200
@@ -71,13 +71,14 @@
 export HGPLAIN=
 
 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 "$?"
+  if [ -f "$ISABELLE_HOME/etc/ISABELLE_ID" ]; then
+    ID="$(cat "$ISABELLE_HOME/etc/ISABELLE_ID")"
+    echo "$ID"
   elif [ -f "$HG_ARCHIVAL" ]; then
     RESULT="$(grep "^node:" < "$HG_ARCHIVAL" | cut -d " " -f2 | head -c12)"
     [ -n "$RESULT" ] && echo "$RESULT"
-  elif [ -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 || exit "$?"
   fi
 fi
 

--- a/lib/scripts/getsettings	Wed Mar 31 17:15:54 2021 +0200
+++ b/lib/scripts/getsettings	Wed Mar 31 18:12:46 2021 +0200
@@ -72,7 +72,6 @@
 fi
 
 #Isabelle distribution identifier -- filled in automatically!
-ISABELLE_ID=""
 [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
 
 

--- a/src/Pure/Admin/build_release.scala	Wed Mar 31 17:15:54 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed Mar 31 18:12:46 2021 +0200
@@ -27,12 +27,14 @@
     val dist_version: String,
     val ident: String)
   {
-    val isabelle_dir: Path = dist_dir + Path.explode(dist_name)
+    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_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
     val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
 
     def other_isabelle(dir: Path): Other_Isabelle =
-      Other_Isabelle(dir + Path.explode(dist_name),
+      Other_Isabelle(dir + isabelle,
         isabelle_identifier = dist_name + "-build",
         progress = progress)
 
@@ -52,8 +54,6 @@
 
   private val getsettings_path = Path.explode("lib/scripts/getsettings")
 
-  private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r
-
   def patch_release(release: Release): Unit =
   {
     val dir = release.isabelle_dir
@@ -65,8 +65,7 @@
     }
 
     File.change(dir + getsettings_path,
-      _.replace("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
-       .replace("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
+      _.replace("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
 
     File.change(dir + Path.explode("lib/html/library_index_header.template"),
       _.replace("{ISABELLE}", release.dist_name))
@@ -418,12 +417,11 @@
       val archive_ident =
         Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
           {
-            val getsettings = Path.explode(release.dist_name) + getsettings_path
+            val getsettings = release.isabelle + getsettings_path
             execute_tar(tmp_dir, "-xzf " +
               File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings))
-            split_lines(File.read(tmp_dir + getsettings))
-              .collectFirst({ case ISABELLE_ID(ident) => ident })
-              .getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive))
+            Isabelle_System.isabelle_id(root = tmp_dir + release.isabelle)
+              .getOrElse(error("Failed to determine ISABELLE_ID from " + release.isabelle_archive))
           })
 
       if (release.ident != archive_ident) {
@@ -451,6 +449,8 @@
 
       progress.echo_warning("Preparing distribution " + quote(release.dist_name))
 
+      File.write(release.isabelle_id, release.ident)
+
       patch_release(release)
 
       if (proper_release_name.isEmpty) make_announce(release)

--- a/src/Pure/General/mercurial.scala	Wed Mar 31 17:15:54 2021 +0200
+++ b/src/Pure/General/mercurial.scala	Wed Mar 31 18:12:46 2021 +0200
@@ -29,6 +29,24 @@
   def opt_template(s: String): String = optional(s, "--template")
 
 
+  /* repository archives */
+
+  private val Archive_Node = """^node: (\S{12}).*$""".r
+
+  sealed case class Archive_Info(lines: List[String])
+  {
+    def id: Option[String] = lines.collectFirst({ case Archive_Node(a) => a })
+  }
+
+  def archive_info(root: Path): Option[Archive_Info] =
+  {
+    val path = root + Path.explode(".hg_archival.txt")
+    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)
+
+
   /* repository access */
 
   def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean =

--- a/src/Pure/System/isabelle_system.scala	Wed Mar 31 17:15:54 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Mar 31 18:12:46 2021 +0200
@@ -156,7 +156,7 @@
   }
 
 
-  /* getenv */
+  /* getenv -- dynamic process environment */
 
   private def getenv_error(name: String): Nothing =
     error("Undefined Isabelle environment variable: " + quote(name))
@@ -170,9 +170,30 @@
 
   def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
 
-  def isabelle_id(): String =
-    proper_string(getenv("ISABELLE_ID")) getOrElse
-      Mercurial.repository(Path.explode("~~")).parent()
+
+  /* getetc -- static distribution parameters */
+
+  def getetc(name: String, root: Path = Path.explode("~~")): Option[String] =
+  {
+    val path = root + Path.basic("etc") + Path.basic(name)
+    if (path.is_file) {
+      Library.trim_split_lines(File.read(path)) match {
+        case Nil => None
+        case List(s) => Some(s)
+        case _ => error("Single line expected in " + path.absolute)
+      }
+    }
+    else None
+  }
+
+
+  /* Isabelle distribution identifier */
+
+  def isabelle_id(root: Path = Path.explode("~~")): Option[String] =
+    getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) orElse {
+      if (Mercurial.is_repository(root)) Some(Mercurial.repository(root).parent())
+      else None
+    }