# HG changeset patch
# User wenzelm
# Date 878307719 -3600
# Node ID 69892b85f800aea6905319b45419aa6933ca1e6a
# Parent  b33e02b3478efcdd246bf550514bc76ba920df6c
Session, Context;

diff -r b33e02b3478e -r 69892b85f800 src/Pure/Thy/ROOT.ML
--- a/src/Pure/Thy/ROOT.ML	Fri Oct 31 15:21:32 1997 +0100
+++ b/src/Pure/Thy/ROOT.ML	Fri Oct 31 15:21:59 1997 +0100
@@ -20,7 +20,36 @@
 open ThmDatabase ThyRead ThyInfo BrowserInfo SymbolInput;
 
 
-(* FIXME tmp *)
+
+(* FIXME tmp, move *)
+
+structure Session =
+struct
+
+local
+  val current_session = ref ([]: string list);
+in
+  fun get_session () = ! current_session;
+  fun add_session s =
+    (current_session := ! current_session @ [s];
+      writeln ("This is the " ^ quote (space_implode "/" (get_session ())) ^ " session."));
+end;
+
+end;
 
-fun set_session s =
-  writeln ("This is the " ^ quote s ^ " session.");
+open Session
+
+
+structure Context =
+struct
+
+local
+  val current_thy = ref ProtoPure.thy;
+in
+  fun context thy = current_thy := thy;
+  fun get_context () = ! current_thy;
+end;
+
+end;
+
+open Context;