# HG changeset patch
# User wenzelm
# Date 1617907939 -7200
# Node ID c54a9395ad96019193861f120b5c0c9916a9dcd6
# Parent  7cb3fefef79e7badc1820f4c9ed01419f9019df7# Parent  a7aabdf889b7105b3ff50df1b3783b256c7f0f58
merged

diff -r 7cb3fefef79e -r c54a9395ad96 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Apr 08 12:38:18 2021 +0000
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Apr 08 20:52:19 2021 +0200
@@ -975,8 +975,7 @@
             Export.export thy (Path.binding (prv_path, Position.none))
               (proved'' |> map (fn (s, _) =>
                 XML.Text (snd (strip_number s) ^
-                  " -- proved by Isabelle/" ^ Isabelle_System.isabelle_id () ^
-                  Isabelle_System.isabelle_heading () ^ "\n")));
+                  " -- proved by " ^ Isabelle_System.identification () ^ "\n")));
         in {pfuns = pfuns, type_map = type_map, env = NONE} end))
   |> Sign.parent_path;
 
diff -r 7cb3fefef79e -r c54a9395ad96 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Apr 08 12:38:18 2021 +0000
+++ b/src/Pure/General/http.scala	Thu Apr 08 20:52:19 2021 +0200
@@ -279,8 +279,7 @@
   def welcome(root: String = "/"): Handler =
     Handler.get(root, arg =>
       if (arg.uri.toString == root) {
-        val id = Isabelle_System.isabelle_id()
-        Some(Response.text("Welcome to Isabelle/" + id + Isabelle_System.isabelle_heading()))
+        Some(Response.text("Welcome to " + Isabelle_System.identification()))
       }
       else None)
 
diff -r 7cb3fefef79e -r c54a9395ad96 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Thu Apr 08 12:38:18 2021 +0000
+++ b/src/Pure/System/isabelle_system.ML	Thu Apr 08 20:52:19 2021 +0200
@@ -25,6 +25,7 @@
   val isabelle_identifier: unit -> string option
   val isabelle_heading: unit -> string
   val isabelle_name: unit -> string
+  val identification: unit -> string
 end;
 
 structure Isabelle_System: ISABELLE_SYSTEM =
@@ -133,4 +134,6 @@
 
 fun isabelle_name () = getenv_strict "ISABELLE_NAME";
 
+fun identification () = "Isabelle/" ^ isabelle_id () ^ isabelle_heading ();
+
 end;
diff -r 7cb3fefef79e -r c54a9395ad96 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Apr 08 12:38:18 2021 +0000
+++ b/src/Pure/System/isabelle_system.scala	Thu Apr 08 20:52:19 2021 +0200
@@ -220,6 +220,8 @@
 
   def isabelle_name(): String = getenv_strict("ISABELLE_NAME")
 
+  def identification(): String = "Isabelle/" + isabelle_id() + isabelle_heading()
+
 
   /** file-system operations **/