Global theory context (used to be in Thy/context.ML);
authorwenzelm
Wed Feb 03 16:40:42 1999 +0100 (1999-02-03)
changeset 618511bf7a8b6a02
parent 6184 8d7a328e2d0c
child 6186 72abe86d9418
Global theory context (used to be in Thy/context.ML);
src/Pure/context.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/context.ML	Wed Feb 03 16:40:42 1999 +0100
     1.3 @@ -0,0 +1,56 @@
     1.4 +(*  Title:      Pure/context.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Global theory context.
     1.9 +*)
    1.10 +
    1.11 +signature BASIC_CONTEXT =
    1.12 +sig
    1.13 +  val context: theory -> unit
    1.14 +  val the_context: unit -> theory
    1.15 +end;
    1.16 +
    1.17 +signature CONTEXT =
    1.18 +sig
    1.19 +  include BASIC_CONTEXT
    1.20 +  val get_context: unit -> theory option
    1.21 +  val set_context: theory option -> unit
    1.22 +  val reset_context: unit -> unit
    1.23 +  val setmp: theory -> ('a -> 'b) -> 'a -> 'b
    1.24 +  val >> : (theory -> theory) -> unit
    1.25 +end;
    1.26 +
    1.27 +structure Context: CONTEXT =
    1.28 +struct
    1.29 +
    1.30 +
    1.31 +(* theory context *)
    1.32 +
    1.33 +local
    1.34 +  val current_theory = ref (None: theory option);
    1.35 +in
    1.36 +  fun get_context () = ! current_theory;
    1.37 +  fun set_context opt_thy = current_theory := opt_thy;
    1.38 +  fun setmp thy f x = Library.setmp current_theory (Some thy) f x;
    1.39 +end;
    1.40 +
    1.41 +fun the_context () =
    1.42 +  (case get_context () of
    1.43 +    Some thy => thy
    1.44 +  | _ => error "Unknown theory context");
    1.45 +
    1.46 +fun context thy = set_context (Some thy);
    1.47 +fun reset_context () = set_context None;
    1.48 +
    1.49 +
    1.50 +(* map context *)
    1.51 +
    1.52 +nonfix >>;
    1.53 +fun >> f = set_context (Some (f (the_context ())));
    1.54 +
    1.55 +
    1.56 +end;
    1.57 +
    1.58 +structure BasicContext: BASIC_CONTEXT = Context;
    1.59 +open BasicContext;