From 4ba652d65269628faf6c81269276c7f9f2c8e60a Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 20 May 2011 08:50:16 +0000
Subject: [PATCH] Simplified rendering.

---
 matitaB/matita/applyTransformation.ml | 46 ++++++++++++++++++---------
 1 file changed, 31 insertions(+), 15 deletions(-)

diff --git a/matitaB/matita/applyTransformation.ml b/matitaB/matita/applyTransformation.ml
index 51ac81268..f99c67f8b 100644
--- a/matitaB/matita/applyTransformation.ml
+++ b/matitaB/matita/applyTransformation.ml
@@ -35,8 +35,10 @@
 
 (* $Id$ *)
 
+
 let use_high_level_pretty_printer = ref true;; 
 
+(*
 let to_text to_content to_pres lowlevel ~map_unicode_to_tex size status t =
  if !use_high_level_pretty_printer then
   let content,ids_to_nrefs = to_content status t in
@@ -45,17 +47,25 @@ let to_text to_content to_pres lowlevel ~map_unicode_to_tex size status t =
    BoxPp.render_to_string ~map_unicode_to_tex
     (function x::_ -> x | _ -> assert false) size pres
  else
-  [],lowlevel t
+  [],lowlevel t *)
 
-let ntxt_of_cic_sequent ~metasenv ~subst =
+(* let ntxt_of_cic_sequent ~metasenv ~subst =
  to_text (Interpretations.nmap_sequent ~metasenv ~subst)
   Content2pres.nsequent2pres
-  (fun seq -> (new NCicPp.status)#ppmetasenv ~subst [seq])
+  (fun seq -> (new NCicPp.status)#ppmetasenv ~subst [seq]) *)
+
+let ntxt_of_cic_sequent ~metasenv ~subst 
+    ~map_unicode_to_tex size status m = 
+  let cseq = Interpretations.nmap_sequent status ~metasenv ~subst m in
+  let markup = CicNotationPres.render_sequent status cseq in
+  BoxPp.render_to_string ~map_unicode_to_tex (List.hd) size markup 
 
-let ntxt_of_cic_object ~map_unicode_to_tex =
+let ntxt_of_cic_object ~map_unicode_to_tex _ _ _ = [],"TO DO"
+(*
  to_text Interpretations.nmap_obj Content2pres.nobj2pres ~map_unicode_to_tex
-  (new NCicPp.status)#ppobj
+  (new NCicPp.status)#ppobj *)
 
+(*
 let ntxt_of_cic_term ~metasenv ~subst ~context =
  to_text (Interpretations.nmap_term ~metasenv ~subst ~context)
   (Content2pres.nterm2pres ?prec:None)
@@ -70,29 +80,35 @@ let ntxt_of_cic_subst ~map_unicode_to_tex size status ~metasenv ?use_subst subst
  [],
  "<<<high level printer for subst not implemented; low-level printing:>>>\n" ^
   (new NCicPp.status)#ppsubst ~metasenv ?use_subst subst
+*)
+
 
 class status =
  object(self)
   inherit Interpretations.status
   inherit TermContentPres.status
+  inherit NCicPp.status
+(*
   method ppterm ~context ~subst ~metasenv ?margin ?inside_fix t =
-   snd (ntxt_of_cic_term ~map_unicode_to_tex:true 80 self ~metasenv ~subst
-    ~context t)
+    NCicPp.ppterm ~metasenv ~subst ~context t
 
   method ppcontext ?sep ~subst ~metasenv context =
-   snd (ntxt_of_cic_context ~map_unicode_to_tex:true 80 self ~metasenv ~subst
-    context)
+    NCicPp.ppcontext self ~metasenv ~subst context
 
   method ppsubst ~metasenv ?use_subst subst =
-   snd (ntxt_of_cic_subst ~map_unicode_to_tex:true 80 self ~metasenv ?use_subst
-    subst)
+    NCicPp.ppcontext self ~metasenv subst *)
 
   method ppmetasenv ~subst metasenv =
    String.concat "\n"
     (List.map
-      (fun m -> snd (ntxt_of_cic_sequent ~map_unicode_to_tex:true 80 self
-        ~metasenv ~subst m)) metasenv)
-
+      (fun m -> ntxt_of_cic_sequent ~map_unicode_to_tex:true 80 self
+        ~metasenv ~subst m) metasenv)
+(*
   method ppobj obj =
-   snd (ntxt_of_cic_object ~map_unicode_to_tex:true 80 self obj)
+   snd (ntxt_of_cic_object ~map_unicode_to_tex:true 80 self obj) *)
  end
+
+let ntxt_of_cic_sequent ~metasenv ~subst 
+    ~map_unicode_to_tex size status m = 
+[], ntxt_of_cic_sequent ~metasenv ~subst 
+    ~map_unicode_to_tex size status m 
-- 
2.39.2