X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FapplyTransformation.ml;h=0528a01ce1bcd6b02bcc317fd70d2b54fd383c72;hb=7666f9dddfcaca5671dd25d3cd2095481968c7bf;hp=51ac812683488f6d5e0d6baa940da126d8ced93b;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/matita/applyTransformation.ml b/matitaB/matita/applyTransformation.ml
index 51ac81268..0528a01ce 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 =
+class status uid =
  object(self)
-  inherit Interpretations.status
-  inherit TermContentPres.status
+  inherit Interpretations.status uid
+  inherit TermContentPres.status uid
+  inherit NCicPp.status uid
+(*
   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 50 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