Frama-C API - marker
The style of added entries. Defaults to empty.
Warning must be set before any entry is added.
The style of hovered entries. Defaults to background green.
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 on_shift_click : ('a entry -> unit) -> unit
method on_add : ('a entry -> unit) -> unit
Register with #add
an entry around its pretty-print.
method mark : 'b. 'a -> (Stdlib.Format.formatter -> 'b -> unit) -> Stdlib.Format.formatter -> 'b -> unit
Register the entry around the pretty-printed material.
method add : 'a entry -> unit
Register an entry