--- a/src/HOL/SPARK/Tools/spark_vcs.ML Wed Apr 07 15:46:06 2021 +0000
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Thu Apr 08 16:43:35 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;
--- a/src/Pure/General/http.scala Wed Apr 07 15:46:06 2021 +0000
+++ b/src/Pure/General/http.scala Thu Apr 08 16:43:35 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)
--- a/src/Pure/System/isabelle_system.ML Wed Apr 07 15:46:06 2021 +0000
+++ b/src/Pure/System/isabelle_system.ML Thu Apr 08 16:43:35 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;
--- a/src/Pure/System/isabelle_system.scala Wed Apr 07 15:46:06 2021 +0000
+++ b/src/Pure/System/isabelle_system.scala Thu Apr 08 16:43:35 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 **/