From 740f6bf8c62629ff54f6db57e7fab5daf222df30 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 18 Aug 2011 09:46:05 +0000
Subject: 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
---
 ide/coqide.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'ide')

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
-- 
cgit v1.2.3