1.1 --- a/src/Pure/System/session.ML	Fri Jul 27 12:29:07 2012 +0200
     1.2 +++ b/src/Pure/System/session.ML	Fri Jul 27 12:43:58 2012 +0200
     1.3 @@ -21,25 +21,22 @@
     1.4  structure Session: SESSION =
     1.5  struct
     1.6  
     1.7 -
     1.8  (* session state *)
     1.9  
    1.10  val session = Unsynchronized.ref ([Context.PureN]: string list);
    1.11 -val session_path = Unsynchronized.ref ([]: string list);
    1.12  val session_finished = Unsynchronized.ref false;
    1.13 -val remote_path = Unsynchronized.ref (NONE: Url.T option);
    1.14 +
    1.15 +fun id () = ! session;
    1.16 +fun name () = "Isabelle/" ^ List.last (! session);
    1.17  
    1.18  
    1.19  (* access path *)
    1.20  
    1.21 -fun id () = ! session;
    1.22 +val session_path = Unsynchronized.ref ([]: string list);
    1.23 +val remote_path = Unsynchronized.ref (NONE: Url.T option);
    1.24 +
    1.25  fun path () = ! session_path;
    1.26  
    1.27 -fun str_of [] = Context.PureN
    1.28 -  | str_of elems = space_implode "/" elems;
    1.29 -
    1.30 -fun name () = "Isabelle/" ^ str_of (path ());
    1.31 -
    1.32  
    1.33  (* welcome *)
    1.34  
    1.35 @@ -61,7 +58,7 @@
    1.36    let val sess = ! session @ [s] in
    1.37      (case duplicates (op =) sess of
    1.38        [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
    1.39 -    | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
    1.40 +    | dups => error ("Duplicate session identifiers " ^ commas_quote dups))
    1.41    end;
    1.42  
    1.43