Merge 'pr/191' into trunk

2 files changed, 40 insertions, 0 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index bcdd4da11..b8f49a9c8 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -388,6 +388,36 @@ let tclFOCUS_gen nosuchgoal i j t =
 let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t
 let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
 
+let tclFOCUSLIST l t =
+  let open Proof in
+  Comb.get >>= fun comb ->
+    let n = CList.length comb in
+    (* First, remove empty intervals, and bound the intervals to the number
+       of goals. *)
+    let sanitize (i, j) =
+      if i > j then None
+      else if i > n then None
+      else if j < 1 then None
+      else Some ((max i 1), (min j n))
+    in
+    let l = CList.map_filter sanitize l in
+    match l with
+      | [] -> tclZERO (NoSuchGoals 0)
+      | (mi, _) :: _ ->
+          (* Get the left-most goal to focus. This goal won't move, and we
+             will then place all the other goals to focus to the right. *)
+          let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in
+          (* [CList.goto] returns a zipper, so that
+             [(rev left) @ sub_right = comb]. *)
+          let left, sub_right = CList.goto (mi-1) comb in
+          let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in
+          let sub, right = CList.partitioni p sub_right in
+          let mj = mi - 1 + CList.length sub in
+            Comb.set (CList.rev_append left (sub @ right)) >>
+            tclFOCUS mi mj t
+
+
+
 (** Like {!tclFOCUS} but selects a single goal by name. *)
 let tclFOCUSID id t =
   let open Proof in
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 93ba55c61..bbf2d6bf7 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -239,6 +239,16 @@ val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit
 
 val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
 
+(** [tclFOCUSLIST li t] applies [t] on the list of focused goals
+    described by [li]. Each element of [li] is a pair [(i, j)] denoting
+    the goals numbered from [i] to [j] (inclusive, starting from 1).
+    It will try to apply [t] to all the valid goals in any of these
+    intervals. If the set of such goals is not a single range, then it
+    will move goals such that it is a single range. (So, for
+    instance, [[1, 3-5]; idtac.] is not the identity.)
+    If the set of such goals is empty, it will fail. *)
+val tclFOCUSLIST : (int * int) list -> 'a tactic -> 'a tactic
+
 (** [tclFOCUSID x t] applies [t] on a (single) focused goal like
     {!tclFOCUS}. The goal is found by its name rather than its
     number.*)