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

4 files changed, 51 insertions, 5 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 502b6b8ea3..30c88a11c0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -147,8 +147,7 @@ GEXTEND Gram
       | tac = Tactic.tactic;
         use_dft_tac = [ "." -> false | "..." -> true ] ->
         (fun g ->
-            (* arnaud: attention �à choisir le bon d�éfaut. *)
-            let g = Option.default (SelectNth 1) g in
+            let g = Option.default (Proof_global.get_default_goal_selector ()) g in
             VernacSolve(g,tac,use_dft_tac)) ] ]
   ;
   located_vernac:
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 1ffa8275a4..5345d40e2f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -777,9 +777,7 @@ let rec pr_vernac = function
         | SelectNth i -> int i ++ str":"
         | SelectAll -> str"all" ++ str":"
       in
-      (* arnaud: attention à imprimer correctement en fonction
-         de la (future) option pour le sélecteur par défaut *)
-      (if i = SelectNth 1 then mt() else pr_goal_selector i) ++
+      (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++
       pr_raw_tactic tac
       ++ (if deftac then str ".." else mt ())
   | VernacSolveExistential (i,c) ->
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)