From d3f1cdd3ebec515770d4c2f8a4f7bbc1859e8946 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 11 Mar 2009 09:48:14 +0000
Subject: [PATCH] added margin option to the pp

---
 helm/software/components/ng_kernel/nCicPp.ml  | 8 +++++++-
 helm/software/components/ng_kernel/nCicPp.mli | 1 +
 2 files changed, 8 insertions(+), 1 deletion(-)

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
 
-- 
2.39.2