(* $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
- inherit Interpretations.status
- inherit TermContentPres.status
- end
+ 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)
-let mpres_document pres_box =
- Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
+ method ppsubst ~metasenv ?use_subst subst =
+ snd (ntxt_of_cic_subst ~map_unicode_to_tex:false 80 self ~metasenv ?use_subst
+ subst)
-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
-;;
+ 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