added >> : (theory -> theory) -> unit;
authorwenzelm
Sun Dec 28 14:56:09 1997 +0100 (1997-12-28)
changeset 448648e4fbc03b7c
parent 4485 697972696f71
child 4487 9b4c1db5aca1
added >> : (theory -> theory) -> unit;
src/Pure/Thy/context.ML
     1.1 --- a/src/Pure/Thy/context.ML	Sun Dec 28 14:55:34 1997 +0100
     1.2 +++ b/src/Pure/Thy/context.ML	Sun Dec 28 14:56:09 1997 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  Global contexts: session and theory.
     1.5  *)
     1.6  
     1.7 -signature CONTEXT =
     1.8 +signature BASIC_CONTEXT =
     1.9  sig
    1.10    val get_session: unit -> string list
    1.11    val add_session: string -> unit
    1.12 @@ -15,6 +15,12 @@
    1.13    val reset_context: unit -> unit
    1.14  end;
    1.15  
    1.16 +signature CONTEXT =
    1.17 +sig
    1.18 +  include BASIC_CONTEXT
    1.19 +  val >> : (theory -> theory) -> unit
    1.20 +end;
    1.21 +
    1.22  structure Context: CONTEXT =
    1.23  struct
    1.24  
    1.25 @@ -41,6 +47,12 @@
    1.26  fun reset_context () = current_theory := None;
    1.27  
    1.28  
    1.29 +nonfix >>;
    1.30 +fun >> f = current_theory := Some (f (get_context ()));
    1.31 +
    1.32 +
    1.33  end;
    1.34  
    1.35 -open Context;
    1.36 +
    1.37 +structure BasicContext: BASIC_CONTEXT = Context;
    1.38 +open BasicContext;