Better indentation.

diff --git a/matita/components/content_pres/content2pres.ml b/matita/components/content_pres/content2pres.ml
index 6606b088be10f49c8ae12fa60a3727cd88751a60..d07733a1670676435894cb91528c20c084bafc83 100644 (file)
--- 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 6846c30b5b9e608fe96af08fbb60b740ccf24b19..12fbb07e17b4010b95d16bb809e33220fb60d82c 100644 (file)
--- 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) ->