# HG changeset patch
# User wenzelm
# Date 1343385838 -7200
# Node ID 0a5f598cacec9f42689277103c72d99d7c807dec
# Parent  f31ef1a0285a66d113a4b44cf0b113d08fc870b1
simplified Session.name;

diff -r f31ef1a0285a -r 0a5f598cacec src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Fri Jul 27 12:29:07 2012 +0200
+++ b/src/Pure/System/session.ML	Fri Jul 27 12:43:58 2012 +0200
@@ -21,24 +21,21 @@
 structure Session: SESSION =
 struct
 
-
 (* session state *)
 
 val session = Unsynchronized.ref ([Context.PureN]: string list);
-val session_path = Unsynchronized.ref ([]: string list);
 val session_finished = Unsynchronized.ref false;
-val remote_path = Unsynchronized.ref (NONE: Url.T option);
+
+fun id () = ! session;
+fun name () = "Isabelle/" ^ List.last (! session);
 
 
 (* access path *)
 
-fun id () = ! session;
-fun path () = ! session_path;
+val session_path = Unsynchronized.ref ([]: string list);
+val remote_path = Unsynchronized.ref (NONE: Url.T option);
 
-fun str_of [] = Context.PureN
-  | str_of elems = space_implode "/" elems;
-
-fun name () = "Isabelle/" ^ str_of (path ());
+fun path () = ! session_path;
 
 
 (* welcome *)
@@ -61,7 +58,7 @@
   let val sess = ! session @ [s] in
     (case duplicates (op =) sess of
       [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
-    | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
+    | dups => error ("Duplicate session identifiers " ^ commas_quote dups))
   end;