further clarification of Isabelle distribution identification -- avoid odd patching of sources;

--- a/lib/Tools/version	Wed Mar 31 22:10:56 2021 +0200
+++ b/lib/Tools/version	Wed Mar 31 22:58:17 2021 +0200
@@ -62,7 +62,7 @@
 ## main
 
 if [ -z "$SHORT_ID" -a -z "$TAGS" ]; then
-  echo 'repository version'    # filled in automatically!
+  echo "$ISABELLE_NAME"
 fi
 
 HG_ARCHIVAL="$ISABELLE_HOME/.hg_archival.txt"

--- a/lib/scripts/getsettings	Wed Mar 31 22:10:56 2021 +0200
+++ b/lib/scripts/getsettings	Wed Mar 31 22:58:17 2021 +0200
@@ -71,8 +71,12 @@
   exit 2
 fi
 
-#Isabelle distribution identifier -- filled in automatically!
-[ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
+if [ -z "$ISABELLE_IDENTIFIER" -a -f "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER" ]
+then
+  ISABELLE_IDENTIFIER="$(cat "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER")"
+fi
+
+ISABELLE_NAME="${ISABELLE_IDENTIFIER:-Isabelle}"
 
 
 # components

--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Mar 31 22:10:56 2021 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Mar 31 22:58:17 2021 +0200
@@ -974,7 +974,9 @@
           val _ =
             Export.export thy (Path.binding (prv_path, Position.none))
               (proved'' |> map (fn (s, _) =>
-                XML.Text (snd (strip_number s) ^ " -- proved by " ^ Distribution.version ^ "\n")));
+                XML.Text (snd (strip_number s) ^
+                  " -- proved by Isabelle/" ^ Isabelle_System.isabelle_id () ^
+                  Isabelle_System.isabelle_heading () ^ "\n")));
         in {pfuns = pfuns, type_map = type_map, env = NONE} end))
   |> Sign.parent_path;
 

--- a/src/Pure/Admin/build_release.scala	Wed Mar 31 22:10:56 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed Mar 31 22:58:17 2021 +0200
@@ -32,6 +32,7 @@
     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_identifier: Path = isabelle_dir + Path.explode("etc/ISABELLE_IDENTIFIER")
     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")
 
@@ -54,34 +55,13 @@
 
   /* patch release */
 
-  private val getsettings_path = Path.explode("lib/scripts/getsettings")
-
   def patch_release(release: Release): Unit =
   {
     val dir = release.isabelle_dir
 
-    for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala"))
-    {
-      File.change(dir + Path.explode(name),
-        _.replace("val is_identified = false", "val is_identified = true"))
-    }
-
-    File.change(dir + getsettings_path,
-      _.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))
 
-    for {
-      name <-
-        List(
-          "src/Pure/System/distribution.ML",
-          "src/Pure/System/distribution.scala",
-          "lib/Tools/version") }
-    {
-      File.change(dir + Path.explode(name), _.replace("repository version", release.dist_version))
-    }
-
     File.change(dir + Path.explode("README"),
       _.replace("some repository version of Isabelle", release.dist_version))
   }
@@ -420,7 +400,7 @@
       val archive_ident =
         Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
           {
-            val getsettings = release.isabelle + getsettings_path
+            val getsettings = release.isabelle + Path.explode("lib/scripts/getsettings")
             execute_tar(tmp_dir, "-xzf " +
               File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings))
             Isabelle_System.isabelle_id(root = tmp_dir + release.isabelle)
@@ -454,6 +434,7 @@
 
       File.write(release.isabelle_id, release.ident)
       File.write(release.isabelle_tags, release.tags)
+      File.write(release.isabelle_identifier, release.dist_name)
 
       patch_release(release)
 

--- a/src/Pure/General/http.scala	Wed Mar 31 22:10:56 2021 +0200
+++ b/src/Pure/General/http.scala	Wed Mar 31 22:58:17 2021 +0200
@@ -280,7 +280,7 @@
     Handler.get(root, arg =>
       if (arg.uri.toString == root) {
         val id = Isabelle_System.isabelle_id()
-        Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version))
+        Some(Response.text("Welcome to Isabelle/" + id + Isabelle_System.isabelle_heading()))
       }
       else None)
 

--- a/src/Pure/PIDE/session.ML	Wed Mar 31 22:10:56 2021 +0200
+++ b/src/Pure/PIDE/session.ML	Wed Mar 31 22:58:17 2021 +0200
@@ -27,10 +27,7 @@
 
 fun description () = "Isabelle/" ^ get_name ();
 
-fun welcome () =
-  if Distribution.is_identified then
-    "Welcome to " ^ description () ^ " (" ^ Distribution.version ^ ")"
-  else "Unofficial version of " ^ description () ^ " (" ^ Distribution.version ^ ")";
+fun welcome () = "Welcome to " ^ description () ^ Isabelle_System.isabelle_heading ();
 
 
 (* base syntax *)

--- a/src/Pure/ROOT.ML	Wed Mar 31 22:10:56 2021 +0200
+++ b/src/Pure/ROOT.ML	Wed Mar 31 22:58:17 2021 +0200
@@ -17,7 +17,6 @@
 
 ML_file "ML/ml_init.ML";
 ML_file "ML/ml_system.ML";
-ML_file "System/distribution.ML";
 
 ML_file "General/basics.ML";
 ML_file "General/symbol_explode.ML";

--- a/src/Pure/System/distribution.ML	Wed Mar 31 22:10:56 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(*  Title:      Pure/System/distribution.ML
-    Author:     Makarius
-
-The Isabelle system distribution -- filled-in by makedist.
-*)
-
-structure Distribution =
-struct
-  val version = "repository version";
-  val is_identified = false;
-end;

--- a/src/Pure/System/distribution.scala	Wed Mar 31 22:10:56 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-/*  Title:      Pure/System/distribution.scala
-    Author:     Makarius
-
-The Isabelle system distribution -- filled-in by makedist.
-*/
-
-package isabelle
-
-
-object Distribution
-{
-  val version = "repository version"
-  val is_identified = false
-}

--- a/src/Pure/System/isabelle_system.ML	Wed Mar 31 22:10:56 2021 +0200
+++ b/src/Pure/System/isabelle_system.ML	Wed Mar 31 22:58:17 2021 +0200
@@ -21,6 +21,10 @@
   val rm_tree: Path.T -> unit
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
   val download: string -> Path.T -> unit
+  val isabelle_id: unit -> string
+  val isabelle_identifier: unit -> string option
+  val isabelle_heading: unit -> string
+  val isabelle_name: unit -> string
 end;
 
 structure Isabelle_System: ISABELLE_SYSTEM =
@@ -115,4 +119,18 @@
 fun download url file =
   ignore (Scala.function "download" (cat_strings0 [url, absolute_path file]));
 
+
+(* Isabelle distribution identification *)
+
+fun isabelle_id () = Scala.function "isabelle_id" "";
+
+fun isabelle_identifier () = try getenv_strict "ISABELLE_IDENTIFIER";
+
+fun isabelle_heading () =
+  (case isabelle_identifier () of
+    NONE => ""
+  | SOME version => " (" ^ version ^ ")");
+
+fun isabelle_name () = getenv_strict "ISABELLE_NAME";
+
 end;

--- a/src/Pure/System/isabelle_system.scala	Wed Mar 31 22:10:56 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Mar 31 22:58:17 2021 +0200
@@ -195,6 +195,12 @@
       else None
     }
 
+  object Isabelle_Id extends Scala.Fun("isabelle_id")
+  {
+    val here = Scala_Project.here
+    def apply(arg: String): String = isabelle_id().get
+  }
+
   def isabelle_tags(root: Path = Path.ISABELLE_HOME): String =
     getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse {
       if (Mercurial.is_repository(root)) {
@@ -204,6 +210,16 @@
       else ""
     }
 
+  def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER"))
+
+  def isabelle_heading(): String =
+    isabelle_identifier() match {
+      case None => ""
+      case Some(version) => " (" + version + ")"
+    }
+
+  def isabelle_name(): String = getenv_strict("ISABELLE_NAME")
+
 
   /** file-system operations **/
 

--- a/src/Pure/System/scala.scala	Wed Mar 31 22:10:56 2021 +0200
+++ b/src/Pure/System/scala.scala	Wed Mar 31 22:58:17 2021 +0200
@@ -259,6 +259,7 @@
   Isabelle_System.Copy_File_Base,
   Isabelle_System.Rm_Tree,
   Isabelle_System.Download,
+  Isabelle_System.Isabelle_Id,
   Isabelle_Tool.Isabelle_Tools,
   isabelle.atp.SystemOnTPTP.List_Systems,
   isabelle.atp.SystemOnTPTP.Run_System)

--- a/src/Pure/Thy/presentation.scala	Wed Mar 31 22:10:56 2021 +0200
+++ b/src/Pure/Thy/presentation.scala	Wed Mar 31 22:58:17 2021 +0200
@@ -348,7 +348,7 @@
 
     val title = "Isabelle/" + chapter + " sessions"
     HTML.write_document(dir, "index.html",
-      List(HTML.title(title + " (" + Distribution.version + ")")),
+      List(HTML.title(title + Isabelle_System.isabelle_heading())),
       HTML.chapter(title) ::
        (if (sessions.isEmpty) Nil
         else
@@ -531,7 +531,7 @@
 
     val title = "Session " + session
     HTML.write_document(session_dir, "index.html",
-      List(HTML.title(title + " (" + Distribution.version + ")")),
+      List(HTML.title(title + Isabelle_System.isabelle_heading())),
       html_context.head(title, List(HTML.par(view_links))) ::
         html_context.contents("Theories", theories))
   }

--- a/src/Pure/Tools/server.scala	Wed Mar 31 22:10:56 2021 +0200
+++ b/src/Pure/Tools/server.scala	Wed Mar 31 22:58:17 2021 +0200
@@ -555,7 +555,7 @@
       connection.reply_ok(
         JSON.Object(
           "isabelle_id" -> Isabelle_System.isabelle_id(),
-          "isabelle_version" -> Distribution.version))
+          "isabelle_name" -> Isabelle_System.isabelle_name()))
 
       var finished = false
       while (!finished) {

--- a/src/Pure/build-jars	Wed Mar 31 22:10:56 2021 +0200
+++ b/src/Pure/build-jars	Wed Mar 31 22:58:17 2021 +0200
@@ -131,7 +131,6 @@
   src/Pure/System/bash.scala
   src/Pure/System/command_line.scala
   src/Pure/System/cygwin.scala
-  src/Pure/System/distribution.scala
   src/Pure/System/executable.scala
   src/Pure/System/getopts.scala
   src/Pure/System/isabelle_charset.scala

--- a/src/Tools/VSCode/src/language_server.scala	Wed Mar 31 22:10:56 2021 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Wed Mar 31 22:58:17 2021 +0200
@@ -308,7 +308,7 @@
       try {
         Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options),
           modes = modes, logic = base_info.session).await_startup()
-        reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")")
+        reply_ok("Welcome to Isabelle/" + base_info.session + Isabelle_System.isabelle_heading())
       }
       catch { case ERROR(msg) => reply_error(msg) }
     }