New option Default Goal Selector.

Set Default Goal Selector "all" prefixes all tactics with "all:" if no selector
is specified (it is overridden by 1: for instance).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16983 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 49 insertions, 0 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5e11cfdb2d..2ca95d9584 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -410,6 +410,46 @@ module Bullet = struct
 end
 
 
+(**********************************************************)
+(*                                                        *)
+(*                     Default goal selector              *)
+(*                                                        *)
+(**********************************************************)
+
+
+(* Default goal selector: selector chosen when a tactic is applied
+   without an explicit selector. *)
+let default_goal_selector = ref (Vernacexpr.SelectNth 1)
+let get_default_goal_selector () = !default_goal_selector
+
+let print_goal_selector = function
+  | Vernacexpr.SelectAll -> "all"
+  | Vernacexpr.SelectNth i -> string_of_int i
+
+let parse_goal_selector = function
+  | "all" -> Vernacexpr.SelectAll
+  | i ->
+      let err_msg = "A selector must be \"all\" or a natural number." in
+      begin try
+              let i = int_of_string i in
+              if i < 0 then Errors.error err_msg;
+              Vernacexpr.SelectNth i
+        with Failure _ -> Errors.error err_msg
+      end
+
+let _ =
+  Goptions.declare_string_option {Goptions.
+                                  optsync = true ;
+                                  optdepr = false;
+                                  optname = "default goal selector" ;
+                                  optkey = ["Default";"Goal";"Selector"] ;
+                                  optread = begin fun () -> print_goal_selector !default_goal_selector end;
+                                  optwrite = begin fun n ->
+                                    default_goal_selector := parse_goal_selector n
+                                  end
+                                 }
+
+
 module V82 = struct
   let get_current_initial_conclusions () =
     let { pid; strength; hook; proof } = cur_pstate () in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 867010fb05..b710b4ffe4 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -144,6 +144,15 @@ module Bullet : sig
   val put : Proof.proof -> t -> Proof.proof
 end
 
+
+(**********************************************************)
+(*                                                        *)
+(*                     Default goal selector              *)
+(*                                                        *)
+(**********************************************************)
+
+val get_default_goal_selector : unit -> Vernacexpr.goal_selector
+
 module V82 : sig
   val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list *
   Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key)