diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-04 21:46:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-04 21:55:31 +0100 |
| commit | 153d77d00ccbacf22aa5d70ca2c1cacab2749339 (patch) | |
| tree | 98997d190ad1b45f3096473c1015feae55b64efe /lib/future.mli | |
| parent | 0aba678e885fa53fa649de59eb1d06b4af3a847c (diff) | |
Specializing the Dyn module to each usecase.
Actually, we never mix the various uses of each dynamic type created through
the Dyn module. To enforce this statically, we functorize the Dyn module so
that we recover a fresh instance at each use point.
Diffstat (limited to 'lib/future.mli')
| -rw-r--r-- | lib/future.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/future.mli b/lib/future.mli index adc15e49c..29b71b70a 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -157,10 +157,11 @@ val transactify : ('a -> 'b) -> 'a -> 'b (** Debug: print a computation given an inner printing function. *) val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds +type freeze (* These functions are needed to get rid of side effects. Thy are set for the outermos layer of the system, since they have to deal with the whole system state. *) -val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit +val set_freeze : (unit -> freeze) -> (freeze -> unit) -> unit val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit |