# HG changeset patch # User wenzelm # Date 918056442 -3600 # Node ID 11bf7a8b6a02545606502b96b3e6d420598b4108 # Parent 8d7a328e2d0c9b50b0f895b5e5cb5ab8abd6c585 Global theory context (used to be in Thy/context.ML); diff -r 8d7a328e2d0c -r 11bf7a8b6a02 src/Pure/context.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/context.ML Wed Feb 03 16:40:42 1999 +0100 @@ -0,0 +1,56 @@ +(* Title: Pure/context.ML + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + +Global theory context. +*) + +signature BASIC_CONTEXT = +sig + val context: theory -> unit + val the_context: unit -> theory +end; + +signature CONTEXT = +sig + include BASIC_CONTEXT + val get_context: unit -> theory option + val set_context: theory option -> unit + val reset_context: unit -> unit + val setmp: theory -> ('a -> 'b) -> 'a -> 'b + val >> : (theory -> theory) -> unit +end; + +structure Context: CONTEXT = +struct + + +(* theory context *) + +local + val current_theory = ref (None: theory option); +in + fun get_context () = ! current_theory; + fun set_context opt_thy = current_theory := opt_thy; + fun setmp thy f x = Library.setmp current_theory (Some thy) f x; +end; + +fun the_context () = + (case get_context () of + Some thy => thy + | _ => error "Unknown theory context"); + +fun context thy = set_context (Some thy); +fun reset_context () = set_context None; + + +(* map context *) + +nonfix >>; +fun >> f = set_context (Some (f (the_context ()))); + + +end; + +structure BasicContext: BASIC_CONTEXT = Context; +open BasicContext;