diff options
| author | Hugo Herbelin | 2018-11-19 15:45:05 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-19 08:40:19 +0000 |
| commit | 05e15386fad28f138e6e889c421242c60b9cb39a (patch) | |
| tree | 1377138a93a361186fdcf2c20d94001e4afd586e | |
| parent | 97f973000a11e667b0d5faef9264f4e681bbd8e1 (diff) | |
CoqIDE: Now calling destroy signal via widget_signals.
Thanks to J. Garrigue for the hint.
| -rw-r--r-- | ide/coqide.ml | 4 | ||||
| -rw-r--r-- | ide/preferences.ml | 4 | ||||
| -rw-r--r-- | ide/preferences.mli | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 94778e0c60..0acbef1ad7 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1222,8 +1222,8 @@ let build_ui () = let () = GtkButton.Toolbar.set ~orientation:`HORIZONTAL ~style:`ICONS ~tooltips:true tbar in - let toolbar = new GObj.widget tbar in - let () = vbox#pack toolbar in + let toolbar = new GButton.toolbar tbar in + let () = vbox#pack toolbar#coerce in (* Emacs/PG mode *) NanoPG.init w notebook all_menus; diff --git a/ide/preferences.ml b/ide/preferences.ml index 7e53dee351..ee274b7001 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -73,11 +73,11 @@ object (self) method default = default end -let stick (pref : 'a preference) (obj : #GObj.widget as 'obj) +let stick (pref : 'a preference) (obj : < connect : #GObj.widget_signals ; .. >) (cb : 'a -> unit) = let _ = cb pref#get in let p_id = pref#connect#changed ~callback:(fun v -> cb v) in - let _ = obj#misc#connect#destroy ~callback:(fun () -> pref#connect#disconnect p_id) in + let _ = obj#connect#destroy ~callback:(fun () -> pref#connect#disconnect p_id) in () (** Useful marshallers *) diff --git a/ide/preferences.mli b/ide/preferences.mli index 7de38c651d..8745c2ae91 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -108,6 +108,6 @@ val load_pref : unit -> unit val configure : ?apply:(unit -> unit) -> GWindow.window -> unit val stick : 'a preference -> - (#GObj.widget as 'obj) -> ('a -> unit) -> unit + < connect : #GObj.widget_signals ; .. > -> ('a -> unit) -> unit val use_default_doc_url : string |