diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 15:27:09 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 15:27:09 +0200 |
commit | 01050348ca54a3ac42da954d85b19c331d0c11db (patch) | |
tree | 025286c27b970d1f548785640b362b7ced08d0fb /plugins/ltac | |
parent | 3af594bb07b3faf8d766bb1e9b6bead7cb1081d8 (diff) | |
parent | c0b244260badedf27fe2b66d3c058ad681af4371 (diff) |
Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).
Diffstat (limited to 'plugins/ltac')
-rw-r--r-- | plugins/ltac/g_ltac.ml4 | 11 | ||||
-rw-r--r-- | plugins/ltac/pptactic.ml | 16 | ||||
-rw-r--r-- | plugins/ltac/pptactic.mli | 2 |
3 files changed, 12 insertions, 17 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 2ea0f60eb..86c983bdd 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -388,16 +388,7 @@ let vernac_solve n info tcom b = p,status) in if not status then Feedback.feedback Feedback.AddedAxiom -let pr_range_selector (i, j) = - if Int.equal i j then int i - else int i ++ str "-" ++ int j - -let pr_ltac_selector = function -| SelectNth i -> int i ++ str ":" -| SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ - str "]" ++ str ":" -| SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":" -| SelectAll -> str "all" ++ str ":" +let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector | [ toplevel_selector(s) ] -> [ s ] diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 8a0764975..d8bd16620 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -477,12 +477,14 @@ type 'a extra_genarg_printer = if Int.equal i j then int i else int i ++ str "-" ++ int j - let pr_goal_selector = function - | SelectNth i -> int i ++ str ":" - | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ - str "]" ++ str ":" - | SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":" - | SelectAll -> str "all" ++ str ":" +let pr_goal_selector toplevel = function + | SelectNth i -> int i ++ str ":" + | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":" + | SelectId id -> str "[" ++ Id.print id ++ str "]:" + | SelectAll -> assert toplevel; str "all:" + +let pr_goal_selector ~toplevel s = + (if toplevel then mt () else str "only ") ++ pr_goal_selector toplevel s let pr_lazy = function | General -> keyword "multi" @@ -988,7 +990,7 @@ type 'a extra_genarg_printer = keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> pr_tac (lcomplete,E) t, lcomplete - | TacSelect (s, tac) -> pr_goal_selector s ++ spc () ++ pr_tac ltop tac, latom + | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom | TacAtom (loc,t) -> diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 1f6ebaf44..c79d5b389 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -53,6 +53,8 @@ type pp_tactic = { pptac_prods : grammar_terminals; } +val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t + val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit val pr_with_occurrences : |