From: Enrico Tassi Date: Sun, 14 Dec 2008 11:36:02 +0000 (+0000) Subject: eureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg fd => c ] is X-Git-Tag: make_still_working~4403 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9b09890767aaa93e512324f8e7f13e2cdeebac88;p=helm.git eureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg fd => c ] is now correctly broken if too long --- diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index d6694cbb6..f1ea0b25e 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -145,16 +145,16 @@ let pp_ast0 t k = let mk_case_pattern = function Ast.Pattern (head, href, vars) -> - hvbox true false (ident_w_href href head :: List.map aux_var vars) + hvbox true true (ident_w_href href head :: + List.flatten (List.map (fun x -> [break;x]) (List.map aux_var vars))) | Ast.Wildcard -> builtin_symbol "_" in let patterns' = List.map (fun (lhs, rhs) -> remove_level_info - (hvbox false true [ - hbox false true [ - mk_case_pattern lhs; builtin_symbol "\\Rightarrow" ]; + (hovbox false true [ + mk_case_pattern lhs; break; builtin_symbol "\\Rightarrow"; break; top_pos (k rhs) ])) patterns in