# HG changeset patch
# User wenzelm
# Date 1621804504 -7200
# Node ID 9f205ca4178a4dbc7c2a7541c40865667e24e200
# Parent  6bd747b71bd3a8d618d6801163eef84dbc697589
tuned message, e.g. for Pure bootstrap;

diff -r 6bd747b71bd3 -r 9f205ca4178a src/Pure/PIDE/session.ML
--- a/src/Pure/PIDE/session.ML	Sun May 23 23:00:10 2021 +0200
+++ b/src/Pure/PIDE/session.ML	Sun May 23 23:15:04 2021 +0200
@@ -25,7 +25,7 @@
 
 fun get_name () = Synchronized.value session;
 
-fun description () = "Isabelle/" ^ get_name ();
+fun description () = (case get_name () of "" => "Isabelle" | name => "Isabelle/" ^ name);
 
 fun welcome () = "Welcome to " ^ description () ^ Isabelle_System.isabelle_heading ();