Strict focusing using Default Goal Selector.

We add a [SelectAlreadyFocused] constructor to [goal_selector] (read
"!") which causes a failure when there's not exactly 1 goal and
otherwise is a noop.

Then [Set Default Goal Selector "!".] puts us in "strict focusing"
mode where we can only run tactics if we have only one goal or use a
selector.

Closes #6689.

2 files changed, 15 insertions, 1 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index abda04ff1..62a38fa32 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -101,6 +101,18 @@ let solve ?with_end_tac gi info_lvl tac pr =
       | Some _ -> Proofview.Trace.record_info_trace tac
     in
     let tac = match gi with
+      | Vernacexpr.SelectAlreadyFocused ->
+        let open Proofview.Notations in
+        Proofview.numgoals >>= fun n ->
+        if n == 1 then tac
+        else
+          let e = CErrors.UserError
+              (None,
+               Pp.(str "Expected a single focused goal but " ++
+                   int n ++ str " goals are focused."))
+          in
+          Proofview.tclZERO e
+
       | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
       | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac
       | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index e22d382f7..d6f7c0e93 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -212,6 +212,7 @@ let pr_range_selector (i, j) =
   else Pp.(int i ++ str "-" ++ int j)
 
 let pr_goal_selector = function
+  | Vernacexpr.SelectAlreadyFocused -> Pp.str "!"
   | Vernacexpr.SelectAll -> Pp.str "all"
   | Vernacexpr.SelectNth i -> Pp.int i
   | Vernacexpr.SelectList l ->
@@ -221,9 +222,10 @@ let pr_goal_selector = function
   | Vernacexpr.SelectId id -> Names.Id.print id
 
 let parse_goal_selector = function
+  | "!" -> Vernacexpr.SelectAlreadyFocused
   | "all" -> Vernacexpr.SelectAll
   | i ->
-      let err_msg = "The default selector must be \"all\" or a natural number." in
+      let err_msg = "The default selector must be \"all\" or \"!\" or a natural number." in
       begin try
               let i = int_of_string i in
               if i < 0 then CErrors.user_err Pp.(str err_msg);