efficiency improvement (buffers are now used everywhere)

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index bd5b7f206a4bd1f02404249e5d85d7f35430cbfe..27b46431ed49b1eedf2e3be8f52386e0ecc3fc92 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -210,11 +210,12 @@ let rec ppcontext ~formatter ?(sep="\n") ~subst ~metasenv = function
 let rec ppmetasenv ~formatter ~subst metasenv = function
   | [] -> ()
   | (i,(name, ctx, ty)) :: tl ->
+      F.fprintf formatter "@[<hov 2>";
       let name = match name with Some n -> "("^n^")" | _ -> "" in
       ppcontext ~formatter ~sep:"; " ~subst ~metasenv ctx;
-      F.fprintf formatter " ⊢ ?%d%s : " i name;
+      F.fprintf formatter "@;⊢@;?%d%s :@;" i name;
       ppterm ~formatter ~metasenv ~subst ~context:ctx ty;
-      F.fprintf formatter "\n";
+      F.fprintf formatter "@]@\n";
       ppmetasenv ~formatter ~subst metasenv tl
 ;;
 
@@ -248,39 +249,45 @@ let ppobj ~formatter (u,_,metasenv, subst, o) =
   F.fprintf formatter "\n";
   match o with 
   | NCic.Fixpoint (b, fl, _) -> 
-      F.fprintf formatter "{%s}\n" (NUri.string_of_uri u);
-      F.fprintf formatter "%s" (if b then "let rec " else "let corec ");
-      HExtlib.list_iter_sep ~sep:(fun ()->F.fprintf formatter "\nand ")
+      F.fprintf formatter "{%s}@\n@[<hov 0>" (NUri.string_of_uri u);
+      F.fprintf formatter "@[<hov 2>%s"(if b then "let rec " else "let corec ");
+      HExtlib.list_iter_sep
+       ~sep:(fun () -> F.fprintf formatter "@\n@[<hov 2>and ")
        (fun (_,name,n,ty,bo) ->
-        F.fprintf formatter "%s on %d : " name n;
+        F.fprintf formatter "%s on %d :@;" name n;
         ppterm ~formatter ~metasenv ~subst ~context:[] ty;
-        F.fprintf formatter " :=\n";
-        ppterm ~formatter ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl
+        F.fprintf formatter "@]@;@[<hov 2>:=@;";
+        ppterm ~formatter ~metasenv ~subst ~context:[] ~inside_fix:true bo;
+        F.fprintf formatter "@]") fl;
+        F.fprintf formatter "@]"
   | NCic.Inductive (b, leftno,tyl, _) -> 
-      F.fprintf formatter "{%s} with %d fixed params\n%s"
+      F.fprintf formatter "{%s} with %d fixed params@\n@[<hov 0>@[<hov 2>%s"
        (NUri.string_of_uri u) leftno
        (if b then "inductive " else "coinductive ");
-      HExtlib.list_iter_sep ~sep:(fun ()->F.fprintf formatter "\nand ")
+      HExtlib.list_iter_sep
+        ~sep:(fun () -> F.fprintf formatter "@\n@[<hov 2>and ")
        (fun (_,name,ty,cl) ->
-          F.fprintf formatter "%s: " name;
+          F.fprintf formatter "%s:@;" name;
           ppterm ~formatter ~metasenv ~subst ~context:[] ty;
-          F.fprintf formatter " :=\n";
-          HExtlib.list_iter_sep ~sep:(fun () -> F.fprintf formatter "\n")
+          F.fprintf formatter "@]@;@[<hov 3>:=@;";
+          HExtlib.list_iter_sep ~sep:(fun () -> F.fprintf formatter "@;")
            (fun (_,name,ty) ->
-             F.fprintf formatter "  | %s: " name;
-             ppterm ~formatter ~metasenv ~subst ~context:[] ty)
-           cl
-        ) tyl
+             F.fprintf formatter "| %s: " name;
+             ppterm ~formatter ~metasenv ~subst ~context:[] ty;)
+           cl;
+          F.fprintf formatter "@]"
+        ) tyl ;
+        F.fprintf formatter "@]"
   | NCic.Constant (_,name,None,ty, _) -> 
-     F.fprintf formatter "{%s}\naxiom %s : " (NUri.string_of_uri u) name;
+     F.fprintf formatter "{%s}@\n@[<hov 2>axiom %s :@;" (NUri.string_of_uri u) name;
      ppterm ~formatter ~metasenv ~subst ~context:[] ty;
-     F.fprintf formatter "\n"
+     F.fprintf formatter "@]@\n"
   | NCic.Constant (_,name,Some bo,ty, _) ->
-     F.fprintf formatter "{%s}\ndefinition %s : " (NUri.string_of_uri u) name;
+     F.fprintf formatter "{%s}@\n@[<hov 0>@[<hov 2>definition %s :@;" (NUri.string_of_uri u) name;
      ppterm ~formatter ~metasenv ~subst ~context:[] ty;
-     F.fprintf formatter " := \n";
+     F.fprintf formatter "@]@;@[<hov 2>:=@;";
      ppterm ~formatter ~metasenv ~subst ~context:[] bo;
-     F.fprintf formatter "\n"
+     F.fprintf formatter "@]@\n@]"
 ;;
 
 let ppterm ~context ~subst ~metasenv ?margin ?inside_fix t =