Test pretty printg of declarative tactics

[helm.git] / matita / matita / applyTransformation.ml

diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml
index 6cbad3b505d50cbcbce9ed8ab09075cec69ff0b3..f761a153b5a839df843d61fd9ca21db2abf6fcef 100644 (file)
--- a/matita/matita/applyTransformation.ml
+++ b/matita/matita/applyTransformation.ml
@@ -35,37 +35,76 @@
 
 (* $Id$ *)
 
-let mpres_document pres_box =
-  Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
-
-let nmml_of_cic_sequent status metasenv subst sequent =
-  let content_sequent,ids_to_refs =
-   NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in 
-  let pres_sequent = 
-   Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in
-  let xmlpres = mpres_document pres_sequent in
-   Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
-
-let ntxt_of_cic_sequent ~map_unicode_to_tex size status metasenv subst sequent =
-  let content_sequent,ids_to_refs =
-   NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in 
-  let pres_sequent = 
-   Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in
-  let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in
+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_sequent
-
-let nmml_of_cic_object status obj =
- let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in 
- let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
- let xmlpres = mpres_document pres_sequent in
-  Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
-;;
-
-let ntxt_of_cic_object ~map_unicode_to_tex size status obj =
- let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in 
- let pres_sequent = Content2pres.ncontent2pres ~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
-;;
+    (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(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 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 _ = NotationPp.set_pp_term (fun status y -> snd (notation_pp_term (Obj.magic status) y))