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 ![].

4 files changed, 52 insertions, 53 deletions

diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
index 81109887ba..4ace6e78d2 100644
--- a/coqpp/coqpp_ast.mli
+++ b/coqpp/coqpp_ast.mli
@@ -103,7 +103,7 @@ type classification =
 
 type vernac_rule = {
   vernac_atts : (string * string) list option;
-  vernac_state: string option;
+  vernac_state : string option;
   vernac_toks : ext_token list;
   vernac_class : code option;
   vernac_depr : bool;
@@ -114,6 +114,7 @@ type vernac_ext = {
   vernacext_name : string;
   vernacext_entry : code option;
   vernacext_class : classification;
+  vernacext_state : string option;
   vernacext_rules : vernac_rule list;
 }
 
diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll
index 81ba8ad98c..9c6b78dc98 100644
--- a/coqpp/coqpp_lex.mll
+++ b/coqpp/coqpp_lex.mll
@@ -103,6 +103,7 @@ rule extend = parse
 | "PLUGIN" { PLUGIN }
 | "DEPRECATED" { DEPRECATED }
 | "CLASSIFIED" { CLASSIFIED }
+| "STATE" { STATE }
 | "PRINTED" { PRINTED }
 | "TYPED" { TYPED }
 | "INTERPRETED" { INTERPRETED }
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 8444f3a58c..ad79599cf4 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -357,41 +357,35 @@ let print_atts_right fmt = function
     let nota = match atts with [_] -> "" | _ -> "Attributes.Notations." in
     fprintf fmt "(Attributes.parse %s%a atts)" nota aux atts
 
-let print_body_wrapper fmt r =
-  match r.vernac_state with
-  | Some "proof_stack" ->
-    fprintf fmt "let proof = (%a) ~pstate:st.Vernacstate.proof in { st with Vernacstate.proof }" print_code r.vernac_body
-
-  | Some "open_proof" ->
-    let push = "Some (Proof_global.push ~ontop:st.Vernacstate.proof pstate)" in
-    fprintf fmt "let pstate = (%a) in let proof = %s in { st with Vernacstate.proof }" print_code r.vernac_body push
-
-  | Some "maybe_open_proof" ->
-    let push = "Proof_global.maybe_push ~ontop:st.Vernacstate.proof pstate" in
-    fprintf fmt "let pstate = (%a) in let proof = %s in { st with Vernacstate.proof }" print_code r.vernac_body push
-
-  | Some "proof" ->
-    fprintf fmt "let proof = Vernacentries.modify_pstate ~pstate:st.Vernacstate.proof (%a) in { st with Vernacstate.proof }" print_code r.vernac_body
-
-  | Some "proof_opt_query" ->
-    fprintf fmt "let () = (%a) ~pstate:(Vernacstate.pstate st) in st" print_code r.vernac_body
-
-  | Some "proof_query" ->
-    fprintf fmt "let () = Vernacentries.with_pstate ~pstate:st.Vernacstate.proof (%a) in st" print_code r.vernac_body
-
-  | None ->
-    fprintf fmt "let () = %a in st" print_code r.vernac_body
-
-  | Some x ->
-    fatal ("unsupported state specifier: " ^ x)
-
-let print_body_fun fmt r =
-  fprintf fmt "let coqpp_body %a%a ~st = @[%a@] in "
-    print_binders r.vernac_toks print_atts_left r.vernac_atts print_body_wrapper r
-
-let print_body fmt r =
+let understand_state = function
+  | "proof_stack" -> "VtModifyProofStack", false
+  | "maybe_open_proof" -> "VtMaybeOpenProof", true
+  | "open_proof" -> "VtOpenProof", true
+  | "proof" -> "VtModifyProof", false
+  | "proof_opt_query" -> "VtReadProofOpt", false
+  | "proof_query" -> "VtReadProof", false
+  | s -> fatal ("unsupported state specifier: " ^ s)
+
+let print_body_state state fmt r =
+  let state = match r.vernac_state with Some _ as s -> s | None -> state in
+  match state with
+  | None -> fprintf fmt "Vernacentries.VtDefault (fun () -> %a)" print_code r.vernac_body
+  | Some "CUSTOM" -> print_code fmt r.vernac_body
+  | Some state ->
+    let state, unit_wrap = understand_state state in
+    fprintf fmt "Vernacentries.%s (%s%a)" state (if unit_wrap then "fun () ->" else "")
+      print_code r.vernac_body
+
+let print_body_wrapper state fmt r =
+  fprintf fmt "Vernacentries.interp_functional_vernac (%a)" (print_body_state state) r
+
+let print_body_fun state fmt r =
+  fprintf fmt "let coqpp_body %a%a = @[%a@] in "
+    print_binders r.vernac_toks print_atts_left r.vernac_atts (print_body_wrapper state) r
+
+let print_body state fmt r =
   fprintf fmt "@[(%afun %a~atts@ ~st@ -> coqpp_body %a%a ~st)@]"
-    print_body_fun r print_binders r.vernac_toks
+    (print_body_fun state) r print_binders r.vernac_toks
     print_binders r.vernac_toks print_atts_right r.vernac_atts
 
 let rec print_sig fmt = function
@@ -402,12 +396,12 @@ let rec print_sig fmt = function
   fprintf fmt "@[Vernacextend.TyNonTerminal (%a, %a)@]"
     print_symbol symb print_sig rem
 
-let print_rule fmt r =
+let print_rule state fmt r =
   fprintf fmt "Vernacextend.TyML (%b, %a, %a, %a)"
-    r.vernac_depr print_sig r.vernac_toks print_body r print_rule_classifier r
+    r.vernac_depr print_sig r.vernac_toks (print_body state) r print_rule_classifier r
 
-let print_rules fmt rules =
-  print_list fmt (fun fmt r -> fprintf fmt "(%a)" print_rule r) rules
+let print_rules state fmt rules =
+  print_list fmt (fun fmt r -> fprintf fmt "(%a)" (print_rule state) r) rules
 
 let print_classifier fmt = function
 | ClassifDefault -> fprintf fmt ""
@@ -426,7 +420,7 @@ let print_ast fmt ext =
   let pr fmt () =
     fprintf fmt "Vernacextend.vernac_extend ~command:\"%s\" %a ?entry:%a %a"
       ext.vernacext_name print_classifier ext.vernacext_class
-      print_entry ext.vernacext_entry print_rules ext.vernacext_rules
+      print_entry ext.vernacext_entry (print_rules ext.vernacext_state) ext.vernacext_rules
   in
   let () = fprintf fmt "let () = @[%a@]@\n" pr () in
   ()
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly
index 43ba990f6a..930a205f85 100644
--- a/coqpp/coqpp_parse.mly
+++ b/coqpp/coqpp_parse.mly
@@ -64,7 +64,7 @@ let parse_user_entry s sep =
 %token <int> INT
 %token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT
 %token RAW_PRINTED GLOB_PRINTED
-%token COMMAND CLASSIFIED PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS
+%token COMMAND CLASSIFIED STATE PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS
 %token BANGBRACKET HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR
 %token LPAREN RPAREN COLON SEMICOLON
 %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA
@@ -183,12 +183,13 @@ argtype:
 ;
 
 vernac_extend:
-| VERNAC vernac_entry EXTEND IDENT vernac_classifier vernac_rules END
+| VERNAC vernac_entry EXTEND IDENT vernac_classifier vernac_state vernac_rules END
   { VernacExt {
     vernacext_name = $4;
     vernacext_entry = $2;
     vernacext_class = $5;
-    vernacext_rules = $6;
+    vernacext_state = $6;
+    vernacext_rules = $7;
   } }
 ;
 
@@ -203,16 +204,21 @@ vernac_classifier:
 | CLASSIFIED AS IDENT { ClassifName $3 }
 ;
 
+vernac_state:
+| { None }
+| STATE IDENT { Some $2 }
+;
+
 vernac_rules:
 | vernac_rule { [$1] }
 | vernac_rule vernac_rules { $1 :: $2 }
 ;
 
 vernac_rule:
-| PIPE vernac_attributes_opt vernac_state_opt LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE
+| PIPE vernac_attributes_opt rule_state LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE
   { {
       vernac_atts = $2;
-      vernac_state= $3;
+      vernac_state = $3;
       vernac_toks = $5;
       vernac_depr = $7;
       vernac_class= $8;
@@ -220,6 +226,11 @@ vernac_rule:
   } }
 ;
 
+rule_state:
+| { None }
+| BANGBRACKET IDENT RBRACKET { Some $2 }
+;
+
 vernac_attributes_opt:
 | { None }
 | HASHBRACKET vernac_attributes RBRACKET { Some $2 }
@@ -236,14 +247,6 @@ vernac_attribute:
 | qualid_or_ident { ($1, $1) }
 ;
 
-vernac_state_opt:
-| { None }
-| BANGBRACKET vernac_state RBRACKET { Some $2 }
-;
-
-vernac_state:
-| qualid_or_ident { $1 }
-
 rule_deprecation:
 | { false }
 | DEPRECATED { true }