From 7d9753115cb26bf27a739e9e1d753fd60b185c17 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 Oct 2009 10:14:36 +0000 Subject: [PATCH] better ppcontext --- helm/software/components/ng_kernel/nCicPp.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) 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 "@["; + ppcontext ~formatter ?sep ~subst ~metasenv c; + F.fprintf formatter "@]"; ;; let ppmetaattrs = -- 2.39.2