Add support for focusing on named goals using brackets.

6 files changed, 53 insertions, 2 deletions

diff --git a/clib/cList.ml b/clib/cList.ml
index de42886dcb..dc59ff2970 100644
--- a/clib/cList.ml
+++ b/clib/cList.ml
@@ -60,6 +60,7 @@ sig
   val extend : bool list -> 'a -> 'a list -> 'a list
   val count : ('a -> bool) -> 'a list -> int
   val index : 'a eq -> 'a -> 'a list -> int
+  val safe_index : 'a eq -> 'a -> 'a list -> int option
   val index0 : 'a eq -> 'a -> 'a list -> int
   val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c
   val fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
@@ -538,6 +539,8 @@ let rec index_f f x l n = match l with
 
 let index f x l = index_f f x l 1
 
+let safe_index f x l = try Some (index f x l) with Not_found -> None
+
 let index0 f x l = index_f f x l 0
 
 (** {6 Folding} *)
diff --git a/clib/cList.mli b/clib/cList.mli
index 42fae5ed39..ed468cb977 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -155,6 +155,10 @@ sig
   val index : 'a eq -> 'a -> 'a list -> int
   (** [index] returns the 1st index of an element in a list (counting from 1). *)
 
+  val safe_index : 'a eq -> 'a -> 'a list -> int option
+  (** [safe_index] returns the 1st index of an element in a list (counting from 1)
+      and None otherwise. *)
+
   val index0 : 'a eq -> 'a -> 'a list -> int
   (** [index0] behaves as [index] except that it starts counting at 0. *)
 
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index 1fdd7317b5..b6654f6d7a 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -23,7 +23,11 @@ let number = [ '0'-'9' ]+
 
 let string = "\"" _+ "\""
 
-let undotted_sep = (number space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+
+let alpha = ['a'-'z' 'A'-'Z']
+
+let ident = alpha (alpha | number | '_' | "'")*
+
+let undotted_sep = ((number | '[' ident ']') space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+
 
 let vernac_control = "Fail" | "Time" | "Redirect" space+ string | "Timeout" space+ number
 
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
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9824172315..5258ab2ea4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1987,8 +1987,9 @@ let vernac_subproof gln =
     match gln with
     | None -> Proof.focus subproof_cond () 1 p
     | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
+    | Some (Goal_select.SelectId id) -> Proof.focus_id subproof_cond () id p
     | _ -> user_err ~hdr:"bracket_selector"
-             (str "Brackets only support the single numbered goal selector."))
+             (str "Brackets do not support multi-goal selectors."))
 
 let vernac_end_subproof () =
   Proof_global.simple_with_current_proof (fun _ p ->