From ec401f51799a051fe8935b36d589fca5a4728d81 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 30 May 2011 16:28:27 +0000 Subject: [PATCH] Better indentation. --- matita/components/content_pres/content2pres.ml | 4 ++-- matita/components/content_pres/termContentPres.ml | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/matita/components/content_pres/content2pres.ml b/matita/components/content_pres/content2pres.ml index 6606b088b..d07733a16 100644 --- a/matita/components/content_pres/content2pres.ml +++ b/matita/components/content_pres/content2pres.ml @@ -1061,13 +1061,13 @@ let nconjlist2pres0 term2pres context = Con.def_id = def_id ; Con.def_term = bo } = d in let r = - Box.b_h [Some "helm", "xref", def_id] + Box.b_hov [Some "helm", "xref", def_id] [ Box.b_object (p_mi [] (match def_name with None -> "_" | Some n -> n)) ; Box.b_space ; Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ; - Box.b_space; term2pres bo] in + Box.indent (term2pres bo)] in aux (r::accum) tl | _::_ -> assert false in diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml index 6846c30b5..12fbb07e1 100644 --- a/matita/components/content_pres/termContentPres.ml +++ b/matita/components/content_pres/termContentPres.ml @@ -143,7 +143,7 @@ let pp_ast0 status t k = in let match_box = hvbox false false [ - hvbox false true [ + hvbox false false [ hvbox false true [keyword "match"; space; break; top_pos (k what)]; break; hvbox false true indty_box; @@ -210,8 +210,8 @@ let pp_ast0 status t k = keyword "let"; space; hvbox false true [ aux_var var; space; - builtin_symbol "\\def"; break; top_pos (k s) ]; - break; space; keyword "in"; space ]; + builtin_symbol "\\def"; break; top_pos (k s); space; keyword "in"; space ]; + ]; break; k t ]) | Ast.LetRec (rec_kind, funs, where) -> -- 2.39.2