X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FapplyTransformation.ml;h=2ae27ee6370f83e717153f6a805acba9b159506d;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hp=236e59def34becbb6654780f2d3f7d42779fbc18;hpb=f9f775a550264a8dc9ce7ea9a48b79892a122c3c;p=helm.git

diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml
index 236e59def..2ae27ee63 100644
--- a/matita/matita/applyTransformation.ml
+++ b/matita/matita/applyTransformation.ml
@@ -35,28 +35,76 @@
 
 (* $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
+  let pres = to_pres status ~ids_to_nrefs content in
+  let pres = CicNotationPres.mpres_of_box pres in
+   BoxPp.render_to_string ~map_unicode_to_tex
+    (function x::_ -> x | _ -> assert false) size pres
+ else
+  [],lowlevel t
+
+let ntxt_of_cic_sequent ~metasenv ~subst =
+ to_text (Interpretations.nmap_sequent ~metasenv ~subst)
+  Content2pres.nsequent2pres
+  (fun seq -> (new NCicPp.status)#ppmetasenv ~subst [seq])
+
+let ntxt_of_cic_object ~map_unicode_to_tex =
+ to_text Interpretations.nmap_cobj Content2pres.nobj2pres ~map_unicode_to_tex
+  (new NCicPp.status)#ppobj
+
+let ntxt_of_cic_term ~metasenv ~subst ~context =
+ to_text (Interpretations.nmap_term ~metasenv ~subst ~context)
+  (Content2pres.nterm2pres ?prec:None)
+  ((new NCicPp.status)#ppterm ~metasenv ~subst ~context)
+
+let ntxt_of_cic_context ~metasenv ~subst =
+ to_text (Interpretations.nmap_context ~metasenv ~subst)
+  Content2pres.ncontext2pres
+  ((new NCicPp.status)#ppcontext ~metasenv ~subst)
+
+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
+ object(self)
   inherit Interpretations.status
   inherit TermContentPres.status
+  method ppterm ~context ~subst ~metasenv ?margin:(_) ?inside_fix:(_) t =
+   snd (ntxt_of_cic_term ~map_unicode_to_tex:false 80 self ~metasenv ~subst
+    ~context t)
+
+  method ppcontext ?sep:(_) ~subst ~metasenv context =
+   snd (ntxt_of_cic_context ~map_unicode_to_tex:false 80 self ~metasenv ~subst
+    context)
+
+  method ppsubst ~metasenv ?use_subst subst =
+   snd (ntxt_of_cic_subst ~map_unicode_to_tex:false 80 self ~metasenv ?use_subst
+    subst)
+
+  method ppmetasenv ~subst metasenv =
+   String.concat "\n"
+    (List.map
+      (fun m -> snd (ntxt_of_cic_sequent ~map_unicode_to_tex:false 80 self
+        ~metasenv ~subst m)) metasenv)
+
+  method ppobj obj =
+   snd (ntxt_of_cic_object ~map_unicode_to_tex:false 80 self obj)
  end
 
-let mpres_document pres_box =
-  Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
+let notation_pp_term status term =
+  let to_pres = Content2pres.nterm2pres ?prec:None in
+  let content = term in
+  let size = 80 in
+  let ids_to_nrefs = Hashtbl.create 1 in
+  let pres = to_pres status ~ids_to_nrefs content in
+  let pres = CicNotationPres.mpres_of_box pres in
+   BoxPp.render_to_string ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+    (function x::_ -> x | _ -> assert false) size pres
 
-let ntxt_of_cic_sequent ~map_unicode_to_tex size status metasenv subst sequent =
-  let content_sequent,ids_to_refs =
-   Interpretations.nmap_sequent status ~metasenv ~subst sequent in 
-  let pres_sequent = 
-   Sequent2pres.nsequent2pres status ids_to_refs subst content_sequent in
-  let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in
-   BoxPp.render_to_string ~map_unicode_to_tex
-    (function x::_ -> x | _ -> assert false) size pres_sequent
-
-let ntxt_of_cic_object ~map_unicode_to_tex size status obj =
- let cobj,ids_to_nrefs = Interpretations.nmap_obj status obj in 
- let pres_sequent = Content2pres.ncontent2pres status ~ids_to_nrefs cobj in
- let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in
-  BoxPp.render_to_string ~map_unicode_to_tex
-   (function x::_ -> x | _ -> assert false) size pres_sequent
-;;
+let _ = NotationPp.set_pp_term (fun status y -> snd (notation_pp_term (Obj.magic status) y))