From c0b244260badedf27fe2b66d3c058ad681af4371 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 26 Sep 2017 14:34:51 +0200
Subject: Properly display the "only" prefix for selectors (bug #5760).

This commit also fixes range selectors being incorrectly displayed.
---
 plugins/ltac/g_ltac.ml4   | 11 +----------
 plugins/ltac/pptactic.ml  | 16 +++++++++-------
 plugins/ltac/pptactic.mli |  2 ++
 3 files changed, 12 insertions(+), 17 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 2ea0f60ebc..86c983bdd9 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 f4e3ba633f..7fe17ceb7b 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 1f6ebaf448..c79d5b389f 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 :
-- 
cgit v1.2.3