+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
+