diff options
| author | letouzey | 2011-08-18 09:46:05 +0000 |
|---|---|---|
| committer | letouzey | 2011-08-18 09:46:05 +0000 |
| commit | 740f6bf8c62629ff54f6db57e7fab5daf222df30 (patch) | |
| tree | 1fa5ff5287afd312d4d4599722707d8ec207cda4 /ide | |
| parent | 50d28541dcb024d8c63fd1b9e770536fc75e325b (diff) | |
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
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 10 |
1 files changed, 4 insertions, 6 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 |