1 files changed, 32 insertions, 27 deletions

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 8162fc3b..23f97612 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Stm
@@ -11,7 +13,7 @@ open Stm
 module Util : sig
 
 val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
-val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ]
 
 type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
 
@@ -23,8 +25,8 @@ val crawl :
 val unit_val : Stm.DynBlockData.t
 val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
 val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
-val of_vernac_expr_val : Vernacexpr.vernac_expr -> Stm.DynBlockData.t
-val to_vernac_expr_val : Stm.DynBlockData.t -> Vernacexpr.vernac_expr
+val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t
+val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control
 
 end = struct
 
@@ -32,7 +34,7 @@ let unit_tag = DynBlockData.create "unit"
 let unit_val = DynBlockData.Easy.inj () unit_tag
 
 let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet"
-let of_vernac_expr_val, to_vernac_expr_val = DynBlockData.Easy.make_dyn "vernac_expr"
+let of_vernac_control_val, to_vernac_control_val = DynBlockData.Easy.make_dyn "vernac_control"
 
 let simple_goal sigma g gs =
   let open Evar in
@@ -43,10 +45,10 @@ let simple_goal sigma g gs =
   Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
   not (List.exists (Proofview.depends_on sigma g) gs)
 
-let is_focused_goal_simple id =
-  match state_of_id id with
+let is_focused_goal_simple ~doc id =
+  match state_of_id ~doc id with
   | `Expired | `Error _ | `Valid None -> `Not
-  | `Valid (Some { proof }) ->
+  | `Valid (Some { Vernacstate.proof }) ->
        let proof = Proof_global.proof_of_state proof in
        let focused, r1, r2, r3, sigma = Proof.proof proof in
        let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
@@ -74,27 +76,29 @@ include Util
 (* ****************** - foo - bar - baz *********************************** *)
 
 let static_bullet ({ entry_point; prev_node } as view) =
-  match entry_point.ast with
+  assert (not (Vernacprop.has_Fail entry_point.ast));
+  match Vernacprop.under_control entry_point.ast with
   | Vernacexpr.VernacBullet b ->
       let base = entry_point.indentation in
       let last_tac = prev_node entry_point in
       crawl view ~init:last_tac (fun prev node ->
         if node.indentation < base then `Stop else
         if node.indentation > base then `Cont node else
-        match node.ast with
+        if Vernacprop.has_Fail node.ast then `Stop
+        else match Vernacprop.under_control node.ast with
         | Vernacexpr.VernacBullet b' when b = b' ->
           `Found { block_stop = entry_point.id; block_start = prev.id;
                    dynamic_switch = node.id; carry_on_data = of_bullet_val b }
         | _ -> `Stop) entry_point
   | _ -> assert false
 
-let dynamic_bullet { dynamic_switch = id; carry_on_data = b } =
-  match is_focused_goal_simple id with
+let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
+  match is_focused_goal_simple ~doc id with
   | `Simple focused ->
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some (Vernacexpr.VernacBullet (to_bullet_val b))
+         recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
       }
   | `Not -> `Leaks
 
@@ -104,9 +108,10 @@ let () = register_proof_block_delimiter
 (* ******************** { block } ***************************************** *)
   
 let static_curly_brace ({ entry_point; prev_node } as view) =
-  assert(entry_point.ast = Vernacexpr.VernacEndSubproof);
+  assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof);
   crawl view (fun (nesting,prev) node ->
-    match node.ast with
+    if Vernacprop.has_Fail node.ast then `Cont (nesting,node)
+    else match Vernacprop.under_control node.ast with
     | Vernacexpr.VernacSubproof _ when nesting = 0 ->
       `Found { block_stop = entry_point.id; block_start = prev.id;
                dynamic_switch = node.id; carry_on_data = unit_val }
@@ -116,13 +121,13 @@ let static_curly_brace ({ entry_point; prev_node } as view) =
       `Cont (nesting + 1,node)
     | _ -> `Cont (nesting,node)) (-1, entry_point)
 
-let dynamic_curly_brace { dynamic_switch = id } =
-  match is_focused_goal_simple id with
+let dynamic_curly_brace doc { dynamic_switch = id } =
+  match is_focused_goal_simple ~doc id with
   | `Simple focused ->
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some Vernacexpr.VernacEndSubproof
+         recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
       }
   | `Not -> `Leaks
 
@@ -138,8 +143,8 @@ let static_par { entry_point; prev_node } =
       Some { block_stop = entry_point.id; block_start = pid;
              dynamic_switch = pid; carry_on_data = unit_val }
 
-let dynamic_par { dynamic_switch = id } =
-  match is_focused_goal_simple id with
+let dynamic_par doc { dynamic_switch = id } =
+  match is_focused_goal_simple ~doc id with
   | `Simple focused ->
       `ValidBlock {
          base_state = id;
@@ -164,19 +169,19 @@ let static_indent ({ entry_point; prev_node } as view) =
         else 
           `Found { block_stop = entry_point.id; block_start = node.id;
                    dynamic_switch = node.id;
-                   carry_on_data = of_vernac_expr_val entry_point.ast }
+                   carry_on_data = of_vernac_control_val entry_point.ast }
         ) last_tac
 
-let dynamic_indent { dynamic_switch = id; carry_on_data = e } =
+let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } =
   Printf.eprintf "%s\n" (Stateid.to_string id);
-  match is_focused_goal_simple id with
+  match is_focused_goal_simple ~doc id with
   | `Simple [] -> `Leaks
   | `Simple focused ->
       let but_last = List.tl (List.rev focused) in 
       `ValidBlock {
          base_state = id;
          goals_to_admit = but_last;
-         recovery_command = Some (to_vernac_expr_val e);
+         recovery_command = Some (to_vernac_control_val e);
       }
   | `Not -> `Leaks