diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 27 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 1 |
2 files changed, 17 insertions, 11 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index e4cba6f07d..5f4a7766f3 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -88,7 +88,7 @@ type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator type pstate = { - pid : Id.t; + pid : Id.t; (* the name of the theorem whose proof is being constructed *) terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; section_vars : Context.Named.t option; @@ -671,16 +671,18 @@ let _ = let default_goal_selector = ref (Vernacexpr.SelectNth 1) let get_default_goal_selector () = !default_goal_selector -let print_range_selector (i, j) = - if i = j then string_of_int i - else string_of_int i ^ "-" ^ string_of_int j +let pr_range_selector (i, j) = + if i = j then int i + else int i ++ str "-" ++ int j -let print_goal_selector = function - | Vernacexpr.SelectAll -> "all" - | Vernacexpr.SelectNth i -> string_of_int i - | Vernacexpr.SelectList l -> "[" ^ - String.concat ", " (List.map print_range_selector l) ^ "]" - | Vernacexpr.SelectId id -> Id.to_string id +let pr_goal_selector = function + | Vernacexpr.SelectAll -> str "all" + | Vernacexpr.SelectNth i -> int i + | Vernacexpr.SelectList l -> + str "[" + ++ prlist_with_sep pr_comma pr_range_selector l + ++ str "]" + | Vernacexpr.SelectId id -> Id.print id let parse_goal_selector = function | "all" -> Vernacexpr.SelectAll @@ -699,7 +701,10 @@ let _ = optdepr = false; optname = "default goal selector" ; optkey = ["Default";"Goal";"Selector"] ; - optread = begin fun () -> print_goal_selector !default_goal_selector end; + optread = begin fun () -> + string_of_ppcmds + (pr_goal_selector !default_goal_selector) + end; optwrite = begin fun n -> default_goal_selector := parse_goal_selector n end diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 3b2cc6b23b..6bb6f5e2cb 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -198,6 +198,7 @@ end (* *) (**********************************************************) +val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds val get_default_goal_selector : unit -> Vernacexpr.goal_selector module V82 : sig |