--- 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;