diff options
| author | Maxime Dénès | 2017-04-24 14:36:45 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-24 14:36:45 +0200 |
| commit | 83d30f7aa8be369a8caf7c130d5dfa4962470eda (patch) | |
| tree | 2919bee50a58ec3810950be43cdb18d96830c0c8 /proofs | |
| parent | ecff95e24e69a8761f7aa154312fdcc01f99766b (diff) | |
| parent | 6c683786c8100259e8c78b710e4a75974ae00eba (diff) | |
Merge PR#565: Remove VernacError
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..61b776f24a 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -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 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_range_selector (i, j) = + if i = j then int i + else int i ++ str "-" ++ int j + +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 |