class type['a]
marker =object
..end
method set_style : GText.tag_property list -> unit
Warning must be set before any entry is added.
method set_hover : GText.tag_property list -> unit
Warning must be set before any entry is added.
method connect : (GdkEvent.Button.t -> 'a entry -> unit) -> unit
method on_click : ('a entry -> unit) -> unit
method on_double_click : ('a entry -> unit) -> unit
method on_right_click : ('a entry -> unit) -> unit
method wrap : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit
#add
an entry around its pretty-print.method mark : 'b. 'a -> (Format.formatter -> 'b -> unit) -> Format.formatter -> 'b -> unit
method add : 'a entry -> unit