- (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 = 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:true 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
+ context)
+
+ method ppsubst ~metasenv ?use_subst subst =
+ snd (ntxt_of_cic_subst ~map_unicode_to_tex:true 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
+ ~metasenv ~subst m)) metasenv)
+
+ method ppobj obj =
+ snd (ntxt_of_cic_object ~map_unicode_to_tex:true 80 self obj)
+ end