src/Pure/Thy/ROOT.ML

 use "thy_read.ML";
 
 open ThmDatabase ThyRead ThyInfo BrowserInfo SymbolInput;
 
 
-(* FIXME tmp *)
 
-fun set_session s =
-  writeln ("This is the " ^ quote s ^ " session.");
+(* 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;
+
+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;