From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 13 Oct 2009 10:14:36 +0000 (+0000)
Subject: better ppcontext
X-Git-Tag: make_still_working~3323
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7d9753115cb26bf27a739e9e1d753fd60b185c17;p=helm.git

better ppcontext
---

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 62dc58e4e..fd9932d9f 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -195,20 +195,25 @@ let ppterm ~formatter ~context ~subst ~metasenv ?(margin=80) ?inside_fix t =
   ppterm ~formatter ~context ~subst ~metasenv ?inside_fix t
 ;;
 
-let rec ppcontext ~formatter ?(sep="\n") ~subst ~metasenv = function
+let rec ppcontext ~formatter ?(sep=";") ~subst ~metasenv = function
   | [] -> ()
   | (name, NCic.Decl t) :: tl -> 
       ppcontext ~formatter ~sep ~subst ~metasenv tl;
       F.fprintf formatter "%s: " name;
       ppterm ~formatter ~subst ~metasenv ~context:tl t;
-      F.fprintf formatter "%s" sep
+      F.fprintf formatter "%s@;" sep
   | (name, NCic.Def (bo,ty)) :: tl->
       ppcontext ~formatter ~sep ~subst ~metasenv tl;
       F.fprintf formatter "%s: " name;
       ppterm ~formatter ~subst ~metasenv ~context:tl ty;
       F.fprintf formatter " := ";
       ppterm ~formatter ~subst ~metasenv ~context:tl bo;
-      F.fprintf formatter "%s" sep
+      F.fprintf formatter "%s@;" sep
+;;
+let ppcontext ~formatter ?sep ~subst ~metasenv c =
+  F.fprintf formatter "@[<hov>";
+  ppcontext ~formatter ?sep ~subst ~metasenv c;
+  F.fprintf formatter "@]";
 ;;
 
 let ppmetaattrs =