From 8baf120d5cf5045d188f7d926162643a6e7ebcd0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 13:46:43 +0200
Subject: STM: proof block detection for par:

"par: tac" is a terminator, if it fails we can admit all focused goals
and continue.
---
 ltac/g_ltac.ml4             |  2 +-
 stm/proofBlockDelimiter.ml  | 22 ++++++++++++++++++++++
 stm/proofBlockDelimiter.mli |  2 ++
 3 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index c8287a2c8d..7c161e5cdc 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -366,7 +366,7 @@ VERNAC tactic_mode EXTEND VernacSolve
     vernac_solve g n t def
   ]
 | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
-    [ VtProofStep{ parallel = true; proof_block_detection = None },
+    [ VtProofStep{ parallel = true; proof_block_detection = Some "par" },
       VtLater ] -> [
     vernac_solve SelectAll n t def
   ]
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 1e37209edd..8c50ad9697 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -125,3 +125,25 @@ let dynamic_curly_brace { dynamic_switch = id } =
 
 let () = register_proof_block_delimiter
   "proof-block" static_curly_brace dynamic_curly_brace
+
+(* ***************** par: ************************************************* *)
+
+let static_par { entry_point; prev_node } =
+  match prev_node entry_point with
+  | None -> None
+  | Some { id = pid } ->
+      Some { stop = entry_point.id; start = pid;
+             dynamic_switch = pid; carry_on_data = unit_val }
+
+let dynamic_par { dynamic_switch = id } =
+  match is_focused_goal_simple id with
+  | `Simple focused ->
+      `ValidBlock {
+         base_state = id;
+         goals_to_admit = focused;
+         recovery_command = None;
+      }
+  | `Not -> `Leaks
+
+let () = register_proof_block_delimiter "par" static_par dynamic_par
+
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
index 8455c18485..a55032a470 100644
--- a/stm/proofBlockDelimiter.mli
+++ b/stm/proofBlockDelimiter.mli
@@ -9,6 +9,7 @@
 (* This file implements proof block detection for:
    - blocks delimited by { and }
    - bullets with indentation
+   - par: terminator
 
    It exports utility functions to ease the development of other proof block
    detection code.
@@ -37,3 +38,4 @@ val unit_val : Stm.DynBlockData.t
 (* Bullets *)
 val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
 val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+
-- 
cgit v1.2.3