From dc664b3b0c6f6f5eeba0c1092efc3f4537cdf657 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 19 Nov 2017 03:40:45 +0100
Subject: [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.
---
 API/API.ml  |  1 +
 API/API.mli | 33 ++++++++++++++++++++-------------
 2 files changed, 21 insertions(+), 13 deletions(-)

(limited to 'API')

diff --git a/API/API.ml b/API/API.ml
index f588fe193a..78d9c0c26e 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -275,6 +275,7 @@ module Command = Command
 module Classes = Classes
 (* module Record *)
 (* module Assumptions *)
+module Vernacstate = Vernacstate
 module Vernacinterp = Vernacinterp
 module Mltop = Mltop
 module Topfmt = Topfmt
diff --git a/API/API.mli b/API/API.mli
index 704f1a3569..8a4a6cc891 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5929,14 +5929,30 @@ sig
     Names.Id.t
 end
 
+module Vernacstate :
+sig
+
+  type t = { (* TODO: inline records in OCaml 4.03 *)
+    system  : States.state;        (* summary + libstack *)
+    proof   : Proof_global.state;  (* proof state *)
+    shallow : bool                 (* is the state trimmed down (libstack) *)
+  }
+
+  (* XXX: This should not be exported *)
+  val freeze_interp_state : Summary.marshallable -> t
+  val unfreeze_interp_state : t -> unit
+
+end
+
 module Vernacinterp :
 sig
+
   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
 
-  val vinterp_add : deprecation -> Vernacexpr.extend_name ->
-    vernac_command -> unit
+  val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit
 
 end
 
@@ -5958,15 +5974,6 @@ end
 module Vernacentries :
 sig
 
-  type interp_state = { (* TODO: inline records in OCaml 4.03 *)
-    system  : States.state;        (* summary + libstack *)
-    proof   : Proof_global.state;  (* proof state *)
-    shallow : bool                 (* is the state trimmed down (libstack) *)
-  }
-
-  val freeze_interp_state : Summary.marshallable -> interp_state
-  val unfreeze_interp_state : interp_state -> unit
-
   val dump_global : Libnames.reference Misctypes.or_by_notation -> unit
   val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
                             Evd.evar_map * Redexpr.red_expr) Hook.t
@@ -5998,7 +6005,7 @@ sig
   val get_doc : Feedback.doc_id -> doc
 
   val state_of_id : doc:doc ->
-    Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ]
+    Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ]
 end
 
 (************************************************************************)
-- 
cgit v1.2.3