# HG changeset patch
# User wenzelm
# Date 1632216198 -7200
# Node ID 7bb0ac635397c20d0927c283aaed51f4ffe1aa14
# Parent  eb54c0604ca5d699c00beecde5099e1dff3b2550
permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone;

diff -r eb54c0604ca5 -r 7bb0ac635397 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Tue Sep 21 00:20:55 2021 +0200
+++ b/src/Pure/System/isabelle_system.ML	Tue Sep 21 11:23:18 2021 +0200
@@ -180,6 +180,7 @@
 
 fun isabelle_name () = getenv_strict "ISABELLE_NAME";
 
-fun identification () = "Isabelle/" ^ isabelle_id () ^ isabelle_heading ();
+fun identification () =
+  "Isabelle" ^ (case try isabelle_id () of SOME id => "/" ^ id | NONE => "") ^ isabelle_heading ();
 
 end;
diff -r eb54c0604ca5 -r 7bb0ac635397 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Sep 21 00:20:55 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Sep 21 11:23:18 2021 +0200
@@ -139,7 +139,8 @@
 
   def isabelle_name(): String = getenv_strict("ISABELLE_NAME")
 
-  def identification(): String = "Isabelle/" + isabelle_id() + isabelle_heading()
+  def identification(): String =
+    "Isabelle" + (try { "/" + isabelle_id () } catch { case ERROR(_) => "" }) + isabelle_heading()
 
 
   /** file-system operations **/