# HG changeset patch
# User wenzelm
# Date 881062664 -3600
# Node ID 68619c232262e266395f5754b5eaa25660036c20
# Parent  062cdcb04b082620d8c3366d3ee309365c26ee0e
Global contexts: session and theory.

diff -r 062cdcb04b08 -r 68619c232262 src/Pure/Thy/context.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/context.ML	Tue Dec 02 12:37:44 1997 +0100
@@ -0,0 +1,40 @@
+(*  Title:      Pure/Thy/context.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Global contexts: session and theory.
+*)
+
+signature CONTEXT =
+sig
+  val get_session: unit -> string list
+  val add_session: string -> unit
+  val reset_session: unit -> unit
+  val get_context: unit -> theory
+  val context: theory -> unit
+end;
+
+structure Context: CONTEXT =
+struct
+
+
+(* session *)
+
+val current_session = ref ([]: string list);
+
+fun get_session () = ! current_session;
+fun add_session s = current_session := ! current_session @ [s];
+fun reset_session () = current_session := [];
+
+
+(* theory context *)
+
+val current_theory = ref ProtoPure.thy;
+
+fun context thy = current_theory := thy;
+fun get_context () = ! current_theory;
+
+
+end;
+
+open Context;