diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-15 20:17:24 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-20 18:26:28 +0100 |
commit | e54d014ce10dea4a74b66e5091d25e4b26bd71fa (patch) | |
tree | bafd7baf26c959f9dabf76edbd518c3536c868e9 /ide/wg_Segment.mli | |
parent | fd8038facfe10abb2c874ca4602b1d2ee0903056 (diff) |
Fixing bug #4540: CoqIDE bottom progress bar does not update.
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 0fc8ebd75..29cbbedac 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 |