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 705ef7936df0b993176d11093c6f03b7104004c7..f761a153b5a839df843d61fd9ca21db2abf6fcef 100644 (file)
--- a/matita/matita/applyTransformation.ml
+++ b/matita/matita/applyTransformation.ml
@@ -76,23 +76,35 @@ class status =
   inherit Interpretations.status
   inherit TermContentPres.status
   method ppterm ~context ~subst ~metasenv ?margin ?inside_fix t =
-   snd (ntxt_of_cic_term ~map_unicode_to_tex:true 80 self ~metasenv ~subst
+   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:true 80 self ~metasenv ~subst
+   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:true 80 self ~metasenv ?use_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:true 80 self
+      (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:true 80 self 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))