From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 11 Mar 2009 09:48:14 +0000 (+0000)
Subject: added margin option to the pp
X-Git-Tag: make_still_working~4161
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d3f1cdd3ebec515770d4c2f8a4f7bbc1859e8946;p=helm.git

added margin option to the pp
---

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 42b05d10e..83422cd8f 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -167,6 +167,12 @@ let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t =
   Buffer.contents buff
 ;;
 
+let ppterm ~context ~subst ~metasenv ?(margin=80) ?inside_fix t = 
+  Format.set_margin margin;
+  ppterm ~context ~subst ~metasenv ?inside_fix t
+;;
+
+
 let ppobj = function
   | (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) -> 
       "{"^NUri.string_of_uri u^"}\n"^
@@ -234,5 +240,5 @@ let rec ppsubst ~subst ~metasenv = function
 
 let ppsubst ~metasenv subst = ppsubst ~metasenv ~subst subst;;
 
-let _ = NCicSubstitution.set_ppterm ppterm;;
+let _ = NCicSubstitution.set_ppterm (ppterm ~margin:80);;
 
diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli
index 507f38d16..bdccdd0fd 100644
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -15,6 +15,7 @@ val ppterm:
   context:NCic.context -> 
   subst:NCic.substitution -> 
   metasenv:NCic.metasenv ->
+  ?margin:int ->
   ?inside_fix:bool ->
    NCic.term -> string