Alternate syntax for ![]: VERNAC EXTEND Foo STATE proof

eg ![proof] becomes STATE proof

This commits still supports the old ![]
so there is redundancy:
~~~
VERNAC EXTEND Foo STATE proof
| ...

VERNAC EXTEND Foo
| ![proof] ...
~~~
with the ![] form being local to the rule and the STATE form
applying to the whole EXTEND except for the rules with a ![].

2 files changed, 49 insertions, 0 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 34b5e13cd8..e4667e376c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2711,3 +2711,39 @@ let interp ?(verbosely=true) ?proof ~st cmd =
     let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in
     Vernacstate.invalidate_cache ();
     iraise exn
+
+(* mlg helpers *)
+
+type functional_vernac =
+  | VtDefault of (unit -> unit)
+  | VtModifyProofStack of (pstate:Proof_global.t option -> Proof_global.t option)
+  | VtMaybeOpenProof of (unit -> Proof_global.pstate option)
+  | VtOpenProof of (unit -> Proof_global.pstate)
+  | VtModifyProof of (pstate:Proof_global.pstate -> Proof_global.pstate)
+  | VtReadProofOpt of (pstate:Proof_global.pstate option -> unit)
+  | VtReadProof of (pstate:Proof_global.pstate -> unit)
+
+let interp_functional_vernac c ~st =
+  let open Proof_global in
+  let open Vernacstate in
+  match c with
+  | VtDefault f -> f (); st
+  | VtModifyProofStack f ->
+    let proof = f ~pstate:st.proof in { st with proof }
+  | VtMaybeOpenProof f ->
+    let pstate = f () in
+    let proof = maybe_push ~ontop:st.proof pstate in
+    { st with proof }
+  | VtOpenProof f ->
+    let pstate = f () in
+    let proof = Some (push ~ontop:st.proof pstate) in
+    { st with proof }
+  | VtModifyProof f ->
+    let proof = modify_pstate f ~pstate:st.proof in
+    { st with proof }
+  | VtReadProofOpt f ->
+    f ~pstate:(Option.map get_current_pstate st.proof);
+    st
+  | VtReadProof f ->
+    with_pstate ~pstate:st.proof f;
+    st
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 5e6e9fdb0f..9756c1e0bb 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -51,3 +51,16 @@ val modify_pstate : pstate:Proof_global.t option -> (pstate:Proof_global.pstate
 (* Flag set when the test-suite is called. Its only effect to display
    verbose information for `Fail` *)
 val test_mode : bool ref
+
+(** For mlg *)
+
+type functional_vernac =
+  | VtDefault of (unit -> unit)
+  | VtModifyProofStack of (pstate:Proof_global.t option -> Proof_global.t option)
+  | VtMaybeOpenProof of (unit -> Proof_global.pstate option)
+  | VtOpenProof of (unit -> Proof_global.pstate)
+  | VtModifyProof of (pstate:Proof_global.pstate -> Proof_global.pstate)
+  | VtReadProofOpt of (pstate:Proof_global.pstate option -> unit)
+  | VtReadProof of (pstate:Proof_global.pstate -> unit)
+
+val interp_functional_vernac : functional_vernac -> st:Vernacstate.t -> Vernacstate.t