# HG changeset patch # User wenzelm # Date 1617224297 -7200 # Node ID 2cd23d587db90f44d55514121a99ea716b104bff # Parent b219774a71ae23d445543988e22b85062d8d331b further clarification of Isabelle distribution identification -- avoid odd patching of sources; diff -r b219774a71ae -r 2cd23d587db9 lib/Tools/version --- 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" diff -r b219774a71ae -r 2cd23d587db9 lib/scripts/getsettings --- 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 diff -r b219774a71ae -r 2cd23d587db9 src/HOL/SPARK/Tools/spark_vcs.ML --- 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; diff -r b219774a71ae -r 2cd23d587db9 src/Pure/Admin/build_release.scala --- 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) diff -r b219774a71ae -r 2cd23d587db9 src/Pure/General/http.scala --- 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) diff -r b219774a71ae -r 2cd23d587db9 src/Pure/PIDE/session.ML --- 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 *) diff -r b219774a71ae -r 2cd23d587db9 src/Pure/ROOT.ML --- 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"; diff -r b219774a71ae -r 2cd23d587db9 src/Pure/System/distribution.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; diff -r b219774a71ae -r 2cd23d587db9 src/Pure/System/distribution.scala --- 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 -} diff -r b219774a71ae -r 2cd23d587db9 src/Pure/System/isabelle_system.ML --- 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; diff -r b219774a71ae -r 2cd23d587db9 src/Pure/System/isabelle_system.scala --- 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 **/ diff -r b219774a71ae -r 2cd23d587db9 src/Pure/System/scala.scala --- 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) diff -r b219774a71ae -r 2cd23d587db9 src/Pure/Thy/presentation.scala --- 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)) } diff -r b219774a71ae -r 2cd23d587db9 src/Pure/Tools/server.scala --- 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) { diff -r b219774a71ae -r 2cd23d587db9 src/Pure/build-jars --- 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 diff -r b219774a71ae -r 2cd23d587db9 src/Tools/VSCode/src/language_server.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) } }