* added group box (?)

[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index e72bfacc8fc8f31da17982b27a0bda3be1b8f78e..436a40571759135d13aa562c0f6bf8518d6f9057 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -93,26 +93,29 @@ let pp_ast0 t k =
   let rec aux = function
     | Ast.Appl ts ->
         Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc),
-          Ast.Layout (Ast.Box ((Ast.HOV, true, true), List.map k ts)))
+          Ast.Layout
+           (Ast.Box ((Ast.HOV, true, true),
+                     (CicNotationUtil.dress
+                        (Ast.Layout Ast.Break)
+                        (List.map k ts)))))
     | Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body)
     | Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) ->
         Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
           Ast.Layout (Ast.Box ((Ast.HV, false, true), [
             aux_ty ty;
-            Ast.Layout (Ast.Box ((Ast.H, false, false), [
-              binder_symbol "\\to";
-              k body]))])))
+           Ast.Layout Ast.Break;                        
+            binder_symbol "\\to";
+            k body])))
     | Ast.Binder (binder_kind, (id, ty), body) ->
         Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
           Ast.Layout (Ast.Box ((Ast.HV, false, true), [
-            Ast.Layout (Ast.Box ((Ast.H, false, false), [
-              binder_symbol (resolve_binder binder_kind);
-              k id;
-              builtin_symbol ":";
-              aux_ty ty ]));
-            Ast.Layout (Ast.Box ((Ast.H, false, false), [
-              builtin_symbol ".";
-              k body ]))])))
+            binder_symbol (resolve_binder binder_kind);
+            k id;
+            builtin_symbol ":";
+            aux_ty ty;
+            Ast.Layout Ast.Break;
+            builtin_symbol ".";
+            k body ])))
     | t -> CicNotationUtil.visit_ast ~special_k k t
   and aux_ty = function
     | None -> builtin_symbol "?"
@@ -265,7 +268,7 @@ let set_compiled32 f = compiled32 := Some f
 
 let instantiate21 env (* precedence associativity *) l1 =
   let rec subst_singleton env t =
-    CicNotationUtil.boxify (subst env t)
+    CicNotationUtil.group (subst env t)
   and subst env = function
     | Ast.AttributedTerm (_, t) -> subst env t
     | Ast.Variable var ->
@@ -296,19 +299,17 @@ let instantiate21 env (* precedence associativity *) l1 =
         let values = CicNotationUtil.ncombine rec_values in
         let sep =
           match sep_opt with
-          | None -> []
-          | Some l -> [ CicNotationPt.Literal l ]
-        in
+            | None -> []
+            | Some l -> [ CicNotationPt.Literal l ]
+       in
         let rec instantiate_list acc = function
           | [] -> List.rev acc
          | value_set :: [] ->
              let env = CicNotationEnv.combine rec_decls value_set in
-               instantiate_list
-                  ((CicNotationUtil.boxify (subst env p)) :: acc) []
+               instantiate_list (CicNotationUtil.group (subst env p) :: acc) []
           | value_set :: tl ->
               let env = CicNotationEnv.combine rec_decls value_set in
-              instantiate_list
-                ((CicNotationUtil.boxify (subst env p @ sep)) :: acc) tl
+               instantiate_list (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl
         in
         instantiate_list [] values
     | Ast.Opt p ->