# HG changeset patch
# User wenzelm
# Date 1199565443 -3600
# Node ID 8a84f00f7139c011d5aa94e10563a361f2a9aa4a
# Parent  54373fa3bd75fa1b9371f139aeb6c97129fa9b74
export session id;

diff -r 54373fa3bd75 -r 8a84f00f7139 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Sat Jan 05 21:37:21 2008 +0100
+++ b/src/Pure/Isar/session.ML	Sat Jan 05 21:37:23 2008 +0100
@@ -7,6 +7,7 @@
 
 signature SESSION =
 sig
+  val id: unit -> string list
   val name: unit -> string
   val welcome: unit -> string
   val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
@@ -28,6 +29,7 @@
 
 (* access path *)
 
+fun id () = ! session;
 fun path () = ! session_path;
 
 fun str_of [] = Context.PureN