1 files changed, 68 insertions, 0 deletions
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
new file mode 100644
index 00000000..65a94a2c
--- /dev/null
+++ b/proofs/goal_select.ml
@@ -0,0 +1,68 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(* spiwack: I'm choosing, for now, to have [goal_selector] be a
+   different type than [goal_reference] mostly because if it makes sense
+   to print a goal that is out of focus (or already solved) it doesn't
+   make sense to apply a tactic to it. Hence it the types may look very
+   similar, they do not seem to mean the same thing. *)
+type t =
+  | SelectAlreadyFocused
+  | SelectNth of int
+  | SelectList of (int * int) list
+  | SelectId of Id.t
+  | SelectAll
+
+(* Default goal selector: selector chosen when a tactic is applied
+   without an explicit selector. *)
+let default_goal_selector = ref (SelectNth 1)
+let get_default_goal_selector () = !default_goal_selector
+
+let pr_range_selector (i, j) =
+  if i = j then Pp.int i
+  else Pp.(int i ++ str "-" ++ int j)
+
+let pr_goal_selector = function
+  | SelectAlreadyFocused -> Pp.str "!"
+  | SelectAll -> Pp.str "all"
+  | SelectNth i -> Pp.int i
+  | SelectList l ->
+    Pp.(str "["
+     ++ prlist_with_sep pr_comma pr_range_selector l
+     ++ str "]")
+  | SelectId id -> Names.Id.print id
+
+let parse_goal_selector = function
+  | "!" -> SelectAlreadyFocused
+  | "all" -> SelectAll
+  | i ->
+      let err_msg = "The default selector must be \"all\" 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);
+              SelectNth i
+        with Failure _ -> CErrors.user_err Pp.(str err_msg)
+      end
+
+let _ = let open Goptions in
+  declare_string_option
+    { optdepr = false;
+      optname = "default goal selector" ;
+      optkey  = ["Default";"Goal";"Selector"] ;
+      optread = begin fun () ->
+        Pp.string_of_ppcmds
+          (pr_goal_selector !default_goal_selector)
+      end;
+      optwrite = begin fun n ->
+        default_goal_selector := parse_goal_selector n
+      end
+    }