From 9eb7f16fc890a1bf3a1332332ed349513905ed66 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Aug 2017 00:35:09 +0200
Subject: Do not thunk notations preemptively.

One has to rely on the 'thunk' token to produce such thunks.
---
 src/tac2core.ml | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

(limited to 'src')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 111ef1c8eb..e0a65dde2d 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -753,7 +753,7 @@ let add_generic_scope s entry arg =
   let parse = function
   | [] ->
     let scope = Extend.Aentry entry in
-    let act x = rthunk (CTacExt (dummy_loc, in_gen (rawwit arg) x)) in
+    let act x = CTacExt (dummy_loc, in_gen (rawwit arg) x) in
     Tac2entries.ScopeRule (scope, act)
   | _ -> scope_fail ()
   in
@@ -818,7 +818,7 @@ end
 let () = add_scope "self" begin function
 | [] ->
   let scope = Extend.Aself in
-  let act tac = rthunk tac in
+  let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
 end
@@ -826,7 +826,7 @@ end
 let () = add_scope "next" begin function
 | [] ->
   let scope = Extend.Anext in
-  let act tac = rthunk tac in
+  let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
 end
@@ -835,12 +835,12 @@ let () = add_scope "tactic" begin function
 | [] ->
   (** Default to level 5 parsing *)
   let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, 5) in
-  let act tac = rthunk tac in
+  let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | [SexprInt (loc, n)] ->
   let () = if n < 0 || n > 5 then scope_fail () in
   let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, n) in
-  let act tac = rthunk tac in
+  let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
 end
@@ -848,7 +848,7 @@ end
 let () = add_scope "ident" begin function
 | [] ->
   let scope = Extend.Aentry Tac2entries.Pltac.q_ident in
-  let act tac = rthunk tac in
+  let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
 end
@@ -856,7 +856,15 @@ end
 let () = add_scope "bindings" begin function
 | [] ->
   let scope = Extend.Aentry Tac2entries.Pltac.q_bindings in
-  let act tac = rthunk tac in
+  let act tac = tac in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "thunk" begin function
+| [tok] ->
+  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+  let act e = rthunk (act e) in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
 end
-- 
cgit v1.2.3