diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /ide/wg_Segment.mli | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'ide/wg_Segment.mli')
-rw-r--r-- | ide/wg_Segment.mli | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli index 0fc8ebd7..29cbbeda 100644 --- a/ide/wg_Segment.mli +++ b/ide/wg_Segment.mli @@ -8,6 +8,8 @@ type color = GDraw.color +type model_event = [ `INSERT | `REMOVE | `SET of int * color ] + class type segment_signals = object inherit GObj.misc_signals @@ -15,15 +17,19 @@ object method clicked : callback:(int -> unit) -> GtkSignal.id end +class type model = +object + method changed : callback:(model_event -> unit) -> unit + method length : int + method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a +end + class segment : unit -> object inherit GObj.widget val obj : Gtk.widget Gtk.obj + method set_model : model -> unit method connect : segment_signals - method length : int - method set_length : int -> unit method default_color : color method set_default_color : color -> unit - method add : int -> color -> unit - method remove : int -> unit end |