equal
deleted
inserted
replaced
23 |
23 |
24 fun init name = Synchronized.change session (K name); |
24 fun init name = Synchronized.change session (K name); |
25 |
25 |
26 fun get_name () = Synchronized.value session; |
26 fun get_name () = Synchronized.value session; |
27 |
27 |
28 fun description () = "Isabelle/" ^ get_name (); |
28 fun description () = (case get_name () of "" => "Isabelle" | name => "Isabelle/" ^ name); |
29 |
29 |
30 fun welcome () = "Welcome to " ^ description () ^ Isabelle_System.isabelle_heading (); |
30 fun welcome () = "Welcome to " ^ description () ^ Isabelle_System.isabelle_heading (); |
31 |
31 |
32 |
32 |
33 (* base syntax *) |
33 (* base syntax *) |