Add support for focusing on named goals using brackets.

2 files changed, 39 insertions, 0 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 51e0a1d614..0d355890c5 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -63,6 +63,7 @@ exception CannotUnfocusThisWay
 (* Cannot focus on non-existing subgoals *)
 exception NoSuchGoals of int * int
 
+exception NoSuchGoal of Names.Id.t
 
 exception FullyUnfocused
 
@@ -75,6 +76,10 @@ let _ = CErrors.register_handler begin function
       CErrors.user_err ~hdr:"Focus" Pp.(
         str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
       )
+  | NoSuchGoal id ->
+      CErrors.user_err
+        ~hdr:"Focus"
+        Pp.(str "No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
   | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused")
   | _ -> raise CErrors.Unhandled
 end
@@ -230,6 +235,37 @@ let focus cond inf i pr =
   try _focus cond (Obj.repr inf) i i pr
   with CList.IndexOutOfRange -> raise (NoSuchGoals (i,i))
 
+(* Focus on the goal named id *)
+let focus_id cond inf id pr =
+  let (focused_goals, evar_map) = Proofview.proofview pr.proofview in
+  begin match try Some (Evd.evar_key id evar_map) with Not_found -> None with
+  | Some ev ->
+     begin match CList.safe_index Evar.equal ev focused_goals with
+     | Some i ->
+        (* goal is already under focus *)
+        _focus cond (Obj.repr inf) i i pr
+     | None ->
+        if CList.mem_f Evar.equal ev pr.shelf then
+          (* goal is on the shelf, put it in focus *)
+          let proofview = Proofview.unshelve [ev] pr.proofview in
+          let shelf =
+            CList.filter (fun ev' -> Evar.equal ev ev' |> not) pr.shelf
+          in
+          let pr = { pr with proofview; shelf } in
+          let (focused_goals, _) = Proofview.proofview pr.proofview in
+          let i =
+            (* Now we know that this will succeed *)
+            try CList.index Evar.equal ev focused_goals
+            with Not_found -> assert false
+          in
+          _focus cond (Obj.repr inf) i i pr
+        else
+          raise CannotUnfocusThisWay
+     end
+  | None ->
+     raise (NoSuchGoal id)
+  end
+
 let rec unfocus kind pr () =
   let cond = cond_of_focus pr in
   match test_cond cond kind pr.proofview with
diff --git a/proofs/proof.mli b/proofs/proof.mli
index c0e832fb8c..33addf13d7 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -137,6 +137,9 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
    a need for it? *)
 val focus : 'a focus_condition -> 'a -> int -> t -> t
 
+(* focus on goal named id *)
+val focus_id : 'aa focus_condition -> 'a -> Names.Id.t -> t -> t
+
 exception FullyUnfocused
 exception CannotUnfocusThisWay