diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 03:40:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 17:38:19 +0100 |
| commit | dc664b3b0c6f6f5eeba0c1092efc3f4537cdf657 (patch) | |
| tree | 228d0aeba91a663b947625fd58cebe5bf4537f08 /vernac/vernacinterp.ml | |
| parent | d7a5f439de0208c4a543a81158107b8ccecb6ced (diff) | |
[plugins] Prepare plugin API for functional handling of state.
To this purpose we allow plugins to register functions that will
modify the state.
This is not used yet, but will be used soon when we remove the global
handling of the proof state.
Diffstat (limited to 'vernac/vernacinterp.ml')
| -rw-r--r-- | vernac/vernacinterp.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index d2687161a..1d024386e 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -11,7 +11,8 @@ open Pp open CErrors type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit +type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> + Vernacstate.t -> Vernacstate.t (* Table of vernac entries *) let vernac_tab = @@ -66,8 +67,9 @@ let call ?locality ?loc (opn,converted_args) = let hunk = callback converted_args in phase := "Executing command"; Locality.LocalityFixme.set locality; - hunk loc; - Locality.LocalityFixme.assert_consumed() + let res = hunk loc in + Locality.LocalityFixme.assert_consumed (); + res with | Drop -> raise Drop | reraise -> |