src/Pure/context.ML
author wenzelm
Tue Mar 09 12:05:07 1999 +0100 (1999-03-09)
changeset 6310 353a8a9d9d2c
parent 6261 6dc692fb3d28
child 8348 ebbbfdb35c84
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/context.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Global theory context.
     6 *)
     7 
     8 signature BASIC_CONTEXT =
     9 sig
    10   val context: theory -> unit
    11   val the_context: unit -> theory
    12 end;
    13 
    14 signature CONTEXT =
    15 sig
    16   include BASIC_CONTEXT
    17   val get_context: unit -> theory option
    18   val set_context: theory option -> unit
    19   val reset_context: unit -> unit
    20   val setmp: theory option -> ('a -> 'b) -> 'a -> 'b
    21   val pass: theory option -> ('a -> 'b) -> 'a -> 'b * theory option
    22   val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
    23   val save: ('a -> 'b) -> 'a -> 'b
    24   val >> : (theory -> theory) -> unit
    25 end;
    26 
    27 structure Context: CONTEXT =
    28 struct
    29 
    30 
    31 (* theory context *)
    32 
    33 local
    34   val current_theory = ref (None: theory option);
    35 in
    36   fun get_context () = ! current_theory;
    37   fun set_context opt_thy = current_theory := opt_thy;
    38   fun setmp opt_thy f x = Library.setmp current_theory opt_thy f x;
    39 end;
    40 
    41 fun the_context () =
    42   (case get_context () of
    43     Some thy => thy
    44   | _ => error "Unknown theory context");
    45 
    46 fun context thy = set_context (Some thy);
    47 fun reset_context () = set_context None;
    48 
    49 fun pass opt_thy f x =
    50   setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x;
    51 
    52 fun pass_theory thy f x =
    53   (case pass (Some thy) f x of
    54     (y, Some thy') => (y, thy')
    55   | (_, None) => error "Missing ML theory context");
    56 
    57 fun save f x = setmp (get_context ()) f x;
    58 
    59 
    60 (* map context *)
    61 
    62 nonfix >>;
    63 fun >> f = set_context (Some (f (the_context ())));
    64 
    65 
    66 end;
    67 
    68 structure BasicContext: BASIC_CONTEXT = Context;
    69 open BasicContext;