added reset_context;
authorwenzelm
Thu, 04 Dec 1997 13:50:18 +0100
changeset 4364 ab73573067d6
parent 4363 b449831f03f4
child 4365 fbb275398eb7
added reset_context;
src/Pure/Thy/context.ML
--- a/src/Pure/Thy/context.ML	Thu Dec 04 13:49:51 1997 +0100
+++ b/src/Pure/Thy/context.ML	Thu Dec 04 13:50:18 1997 +0100
@@ -12,6 +12,7 @@
   val reset_session: unit -> unit
   val get_context: unit -> theory
   val context: theory -> unit
+  val reset_context: unit -> unit
 end;
 
 structure Context: CONTEXT =
@@ -29,10 +30,15 @@
 
 (* theory context *)
 
-val current_theory = ref ProtoPure.thy;
+val current_theory = ref (None: theory option);
 
-fun context thy = current_theory := thy;
-fun get_context () = ! current_theory;
+fun get_context () =
+  (case current_theory of
+    ref (Some thy) => thy
+  | _ => error "Unknown theory context");
+
+fun context thy = current_theory := Some thy;
+fun reset_context () = current_theory := None;
 
 
 end;