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.
---
 grammar/vernacextend.mlp | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

(limited to 'grammar')

diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 874712124c..12308bedef 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -158,18 +158,26 @@ EXTEND
   deprecation:
     [ [ "DEPRECATED" -> () ] ]
   ;
-  (* spiwack: comment-by-guessing: it seems that the isolated string (which
-      otherwise could have been another argument) is not passed to the
-      VernacExtend interpreter function to discriminate between the clauses. *)
+  (* spiwack: comment-by-guessing: it seems that the isolated string
+      (which otherwise could have been another argument) is not passed
+      to the VernacExtend interpreter function to discriminate between
+      the clauses. *)
+
+  (* ejga: Due to the LocalityFixme abomination we cannot eta-expand
+      [e] as we'd like to, so we need to use the below mess with [fun
+      st -> st].
+
+      At some point We should solve the mess and extend
+      vernacextend.mlp with locality info. *)
   rule:
     [ [ "["; s = STRING; l = LIST0 args; "]";
         d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
       let () = if s = "" then failwith "Command name is empty." in
-      let b = <:expr< fun loc -> $e$ >> in
+      let b = <:expr< fun loc -> ( let () = $e$ in fun st -> st ) >> in
       { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
       | "[" ; "-" ; l = LIST1 args ; "]" ;
         d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let b = <:expr< fun loc -> $e$ >> in
+      let b = <:expr< fun loc -> ( let () = $e$ in fun st -> st ) >> in
       { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
     ] ]
   ;
-- 
cgit v1.2.3