+ fun ?(prec=90) ast ->
+ CicNotationPres.box_of_mpres
+ (CicNotationPres.render status ~lookup_uri ~prec
+ (TermContentPres.pp_ast status ast))
+
+let nobj2pres status ~ids_to_nrefs =
+ nobj2pres0 ?skip_initial_lambdas:None ?skip_thm_and_qed:None
+ (nterm2pres status ~ids_to_nrefs)
+
+let nconjlist2pres0 term2pres context =
+ let rec aux accum =
+ function
+ [] -> accum
+ | None::tl -> aux accum tl
+ | (Some (`Declaration d))::tl ->
+ let
+ { Con.dec_name = dec_name ;
+ Con.dec_id = dec_id ;
+ Con.dec_type = ty } = d in
+ let r =
+ Box.b_h [Some "helm", "xref", dec_id]
+ [ Box.b_object (p_mi []
+ (match dec_name with
+ None -> "_"
+ | Some n -> n)) ;
+ Box.b_space; Box.b_text [] ":"; Box.b_space;
+ term2pres ty] in
+ aux (r::accum) tl
+ | (Some (`Definition d))::tl ->
+ let
+ { Con.def_name = def_name ;
+ Con.def_id = def_id ;
+ Con.def_term = bo } = d in
+ let r =
+ Box.b_h [Some "helm", "xref", def_id]
+ [ Box.b_object (p_mi []
+ (match def_name with
+ None -> "_"
+ | Some n -> n)) ; Box.b_space ;
+ Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ;
+ Box.b_space; term2pres bo] in
+ aux (r::accum) tl
+ | _::_ -> assert false
+ in
+ if context <> [] then [Box.b_v [] (aux [] context)] else []
+
+let sequent2pres0 term2pres (_,_,context,ty) =
+ let pres_context = nconjlist2pres0 term2pres context in
+ let pres_goal = term2pres ty in
+ (Box.b_h [] [
+ Box.b_space;
+ (Box.b_v []
+ (Box.b_space ::
+ pres_context @ [
+ b_ink [None,"width","4cm"; None,"height","2px"]; (* sequent line *)
+ Box.b_space;
+ pres_goal]))])
+
+let ncontext2pres status ~ids_to_nrefs ctx =
+ let ctx = HExtlib.filter_map (fun x -> x) ctx in
+ context2pres (nterm2pres status ~ids_to_nrefs) ~continuation:Box.smallskip
+ (ctx:>NotationPt.term Con.in_proof_context_element list)
+
+let nsequent2pres status ~ids_to_nrefs =
+ sequent2pres0 (nterm2pres status ~ids_to_nrefs)