1signature smpp = 2sig 3 4 type ('a,'b) t = 5 'a * HOLPP.pretty list -> ('b * ('a * HOLPP.pretty list)) option 6 7 val add_string : string -> ('a,unit) t 8 val add_stringsz : string * int -> ('a,unit) t 9 val add_newline : ('a,unit) t 10 val add_break : int * int -> ('a,unit) t 11 val nothing : ('a,unit) t 12 val fail : ('a,unit) t 13 val >> : ('a,'b) t * ('a,'c) t -> ('a,'c) t 14 val >- : ('a,'b) t * ('b -> ('a,'c) t) -> ('a,'c) t 15 val || : ('a,'b) t * ('a,'b) t -> ('a,'b) t 16 val ||| : ('a,'b) t * (unit -> ('a,'b) t) -> ('a,'b) t 17 val return : 'b -> ('a,'b) t 18 val fupdate : ('a -> 'a) -> ('a,'a) t 19 20 val block : HOLPP.break_style -> int -> ('a,'b) t -> ('a,'b) t 21 val mapp : ('a -> ('b,unit) t) -> 'a list -> ('b, unit) t 22 val mmap : ('a -> ('b,'c) t) -> 'a list -> ('b, 'c list) t 23 val pr_list : ('b -> ('a,unit)t) -> ('a,unit) t -> 'b list -> ('a,unit)t 24 val mappr_list : ('b -> ('a,'c)t) -> ('a,unit) t -> 'b list -> ('a,'c list) t 25 val lift : ('a -> HOLPP.pretty) -> 'a -> ('st,unit) t 26 val lower : ('st,'a) t -> 'st -> (HOLPP.pretty * 'a * 'st) option 27 28(* 29 val from_backend : 30 PPBackEnd.t -> 31 {add_string : string -> ('a,unit) t, 32 add_xstring : PPBackEnd.xstring -> ('a,unit) t, 33 flush : ('a,unit) t, 34 add_newline : ('a,unit) t, 35 add_break : int * int -> ('a,unit) t, 36 ublock : HOLPP.break_style -> int -> ('a,unit) t -> ('a,unit) t, 37 ustyle : PPBackEnd.pp_style list -> ('a,unit) t -> ('a,unit) t} 38 39 val backend_block : PPBackEnd.t -> HOLPP.break_style -> int -> 40 ('a,'b) t -> ('a,'b) t 41 val backend_style : PPBackEnd.t -> PPBackEnd.pp_style list -> 42 ('a,'b) t -> ('a,'b) t 43*) 44end 45