params
in
B.b_hv []
- [B.b_hv []
- ([ B.b_space; B.b_text [] name; B.b_space ] @ params @
- (if rno <> -1 then [B.b_kw "on" ; B.b_space; term2pres rec_param ] else [])
- @[ B.b_space;
- B.b_text [] ":"; B.b_space; term2pres ty]);
+ [B.b_hov (RenderingAttrs.indent_attributes `BoxML)
+ ( [B.b_hov (RenderingAttrs.indent_attributes `BoxML) ([ B.b_space; B.b_text [] name ] @
+ [B.indent(B.b_hov (RenderingAttrs.indent_attributes `BoxML) (params))])]
+ @ [B.b_h []
+ ((if rno <> -1 then
+ [B.b_kw "on";B.b_space;term2pres rec_param] else [])
+ @ [ B.b_space; B.b_text [] ":";]) ]
+ @[ B.indent(term2pres ty)]);
B.b_text [] ":=";
B.b_h [] [B.b_space;term2pres body] ]
;;
;;
let content2pres0
- ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres
+ ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+ (term2pres : ?prec:int -> 'a)
(id,params,metasenv,obj)
=
match obj with
?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts
=
content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
+(* FG: prec not optional in my patch *)
(fun ?(prec=90) annterm ->
let ast, ids_to_uris =
TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
(TermContentPres.pp_ast ast)))
let ncontent2pres0
- ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres
+ ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+ (term2pres : ?prec:int -> 'a)
(id,params,metasenv,obj : CicNotationPt.term Content.cobj)
=
match obj with