From 3b6baca9f28c7d410e543c19f0d8e8467bf25894 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 11 May 2009 21:45:00 +0000 Subject: [PATCH] Missing spaces inserted here and there. --- .../components/content_pres/termContentPres.ml | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index f1ea0b25e..85f4a3187 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -95,6 +95,11 @@ let string_of_sort_kind = function | `Type _ -> "Type" | `NType s -> "Type[" ^ s ^ "]" +let map_space f l = + HExtlib.list_concat + ~sep:[space] (List.map (fun x -> [f x]) l) +;; + let pp_ast0 t k = let rec aux = function @@ -146,7 +151,7 @@ let pp_ast0 t k = function Ast.Pattern (head, href, vars) -> hvbox true true (ident_w_href href head :: - List.flatten (List.map (fun x -> [break;x]) (List.map aux_var vars))) + List.flatten (List.map (fun x -> [break;x]) (map_space aux_var vars))) | Ast.Wildcard -> builtin_symbol "_" in let patterns' = @@ -205,8 +210,8 @@ let pp_ast0 t k = match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec" in let mk_fun (args, (name,ty), body, rec_param) = - List.map aux_var args ,k name, HExtlib.map_option k ty, k body, - fst (List.nth args rec_param) + List.flatten (List.map (fun x -> [aux_var x; space]) args), + k name, HExtlib.map_option k ty, k body, fst (List.nth args rec_param) in let mk_funs = List.map mk_fun in let fst_fun, tl_funs = @@ -219,9 +224,10 @@ let pp_ast0 t k = space; keyword rec_op; space; - name] @ + name; + space] @ params @ - [space; keyword "on" ; space ; rec_param ;space ] @ + [keyword "on" ; space ; rec_param ;space ] @ (match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @ [ builtin_symbol "\\def"; break; -- 2.39.2