From d94fef210a63db4ff34251afe093041912a7cbde Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 8 Mar 2018 12:45:37 +0100
Subject: 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.
---
 plugins/ltac/g_ltac.ml4  | 1 +
 plugins/ltac/pptactic.ml | 1 +
 plugins/ltac/tacexpr.ml  | 1 +
 plugins/ltac/tacexpr.mli | 1 +
 4 files changed, 4 insertions(+)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 0c42a8bb2..a1d7d9b1a 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -325,6 +325,7 @@ GEXTEND Gram
   ;
   toplevel_selector:
     [ [ sel = selector_body; ":" -> sel
+    |   "!"; ":" -> SelectAlreadyFocused
     |   IDENT "all"; ":" -> SelectAll ] ]
   ;
   tactic_mode:
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 11bb7a234..bd02d85d5 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -515,6 +515,7 @@ let string_of_genarg_arg (ArgumentType arg) =
     else int i ++ str "-" ++ int j
 
 let pr_goal_selector toplevel = function
+  | SelectAlreadyFocused -> str "!:"
   | SelectNth i -> int i ++ str ":"
   | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":"
   | SelectId id -> str "[" ++ Id.print id ++ str "]:"
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 3baa475ab..37abfeee9 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -36,6 +36,7 @@ type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
 
 type goal_selector = Vernacexpr.goal_selector =
+  | SelectAlreadyFocused
   | SelectNth of int
   | SelectList of (int * int) list
   | SelectId of Id.t
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 3baa475ab..37abfeee9 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -36,6 +36,7 @@ type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
 
 type goal_selector = Vernacexpr.goal_selector =
+  | SelectAlreadyFocused
   | SelectNth of int
   | SelectList of (int * int) list
   | SelectId of Id.t
-- 
cgit v1.2.3