Misc improvements concerning "Show Match" and its coqide equivalent

 - The make_cases function was duplicated in two files
 - Rather use next_name_away_in_cases_pattern instead of ..._in_goal
   when finding fresh pattern variables
 - Nicer final pretty-print via some formatting boxes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14414 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 37 insertions, 69 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 5c757d9711..be0b528e7a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2194,16 +2194,14 @@ let main files =
       match Coq.make_cases cur_ct w with
         | Ide_intf.Fail _ -> raise Not_found
         | Ide_intf.Good cases ->
-          let print c = function
-            | [x] -> Format.fprintf c "  | %s => _@\n" x
-            | x::l -> Format.fprintf c "  | (%s%a) => _@\n" x
-              (print_list (fun c s -> Format.fprintf c " %s" s)) l
-            | [] -> assert false
+          let print_branch c l =
+	    Format.fprintf c " | @[<hov 1>%a@]=> _@\n"
+	      (print_list (fun c s -> Format.fprintf c "%s@ " s)) l
           in
           let b = Buffer.create 1024 in
           let fmt = Format.formatter_of_buffer b in
           Format.fprintf fmt "@[match var with@\n%aend@]@."
-            (print_list print) cases;
+            (print_list print_branch) cases;
           let s = Buffer.contents b in
           prerr_endline s;
           let {script = view } = session_notebook#current_term in
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 0a96e4d667..bd92460f24 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -34,7 +34,9 @@ val rewind : int -> unit call
 (** Is a file present somewhere in Coq's loadpath ? *)
 val is_in_loadpath : string -> bool call
 
-(** Create a "match" template for a given inductive type *)
+(** Create a "match" template for a given inductive type.
+    For each branch of the match, we list the constructor name
+    followed by enough pattern variables. *)
 val make_cases : string -> string list list call
 
 (** The status, for instance "Ready in SomeSection, proving Foo" *)
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 4d1574e8c3..c7667f0300 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -430,40 +430,6 @@ let current_goals () =
   with Proof_global.NoCurrentProof ->
     Ide_intf.Message "" (* quick hack to have a clean message screen *)
 
-let id_of_name = function
-  | Names.Anonymous -> id_of_string "x"
-  | Names.Name x -> x
-
-let make_cases s =
-  let qualified_name = Libnames.qualid_of_string s in
-  let glob_ref = Nametab.locate qualified_name in
-  match glob_ref with
-    | Libnames.IndRef i ->
-        let {Declarations.mind_nparams = np},
-            {Declarations.mind_consnames = carr ;
-             Declarations.mind_nf_lc = tarr }
-              = Global.lookup_inductive i
-        in
-        Util.array_fold_right2
-          (fun n t l ->
-             let (al,_) = Term.decompose_prod t in
-             let al,_ = Util.list_chop (List.length al - np) al in
-             let rec rename avoid = function
-               | [] -> []
-               | (n,_)::l ->
-                   let n' = next_ident_away_in_goal
-                              (id_of_name n)
-                              avoid
-                   in (string_of_id n')::(rename (n'::avoid) l)
-             in
-             let al' = rename [] (List.rev al) in
-             (string_of_id n :: al') :: l
-          )
-          carr
-          tarr
-          []
-    | _ -> raise Not_found
-
 let current_status () =
   (** We remove the initial part of the current [dir_path]
       (usually Top in an interactive session, cf "coqtop -top"),
@@ -539,7 +505,7 @@ let eval_call c =
     Ide_intf.read_stdout = interruptible read_stdout;
     Ide_intf.current_goals = interruptible current_goals;
     Ide_intf.current_status = interruptible current_status;
-    Ide_intf.make_cases = interruptible make_cases }
+    Ide_intf.make_cases = interruptible Vernacentries.make_cases }
   in
   Ide_intf.abstract_eval_call handler handle_exn c
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c42d7acf64..b5484d40f3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -110,13 +110,12 @@ let show_intro all =
       msgnl (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
     with Failure "list_last" -> message ""
 
-let id_of_name = function
-  | Names.Anonymous -> id_of_string "x"
-  | Names.Name x -> x
+(** Prepare a "match" template for a given inductive type.
+    For each branch of the match, we list the constructor name
+    followed by enough pattern variables.
+    [Not_found] is raised if the given string isn't the qualid of
+    a known inductive type. *)
 
-
-(* Building of match expression *)
-(* From ide/coq.ml *)
 let make_cases s =
   let qualified_name = Libnames.qualid_of_string s in
   let glob_ref = Nametab.locate qualified_name in
@@ -126,36 +125,31 @@ let make_cases s =
 	    , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr }
 	      = Global.lookup_inductive i in
 	Util.array_fold_right2
-	  (fun n t l ->
-	     let (al,_) = Term.decompose_prod t in
-	     let al,_ = Util.list_chop (List.length al - np) al in
+	  (fun consname typ l ->
+	     let al = List.rev (fst (Term.decompose_prod typ)) in
+	     let al = Util.list_skipn np al in
 	     let rec rename avoid = function
 	       | [] -> []
 	       | (n,_)::l ->
-		   let n' = Namegen.next_ident_away_in_goal (id_of_name n) avoid in
+		   let n' = Namegen.next_name_away_in_cases_pattern n avoid in
 		   string_of_id n' :: rename (n'::avoid) l in
-	     let al' = rename [] (List.rev al) in
-	     (string_of_id n :: al') :: l)
+	     let al' = rename [] al in
+	     (string_of_id consname :: al') :: l)
 	  carr tarr []
     | _ -> raise Not_found
 
+(** Textual display of a generic "match" template *)
 
 let show_match id =
-  try
-    let s = string_of_id (snd id) in
-    let patterns = List.rev (make_cases s) in
-    let cases =
-      List.fold_left
-	(fun acc x ->
-	  match x with
-	    | [] -> assert false
-	    | [x] -> "| "^ x  ^ " => \n" ^ acc
-	    | x::l ->
-		"| " ^ List.fold_left (fun acc s ->  acc ^ " " ^ s) x l
-		^ " => \n" ^ acc)
-	"end" patterns in
-    msg (str ("match # with\n" ^ cases))
-  with Not_found -> error "Unknown inductive type."
+  let patterns =
+    try make_cases (string_of_id (snd id))
+    with Not_found -> error "Unknown inductive type."
+  in
+  let pr_branch l =
+    str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>"
+  in
+  msg (v 1 (str "match # with" ++ fnl () ++
+	    prlist_with_sep fnl pr_branch patterns ++ fnl ()))
 
 (* "Print" commands *)
 
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 69684b78c8..02cfa85344 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -56,3 +56,11 @@ val vernac_reset_name : identifier Util.located -> unit
 (* Print subgoals when the verbose flag is on. Meant to be used inside
     vernac commands from plugins. *)
 val print_subgoals : unit -> unit
+
+(** Prepare a "match" template for a given inductive type.
+    For each branch of the match, we list the constructor name
+    followed by enough pattern variables.
+    [Not_found] is raised if the given string isn't the qualid of
+    a known inductive type. *)
+
+val make_cases : string -> string list list