diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-01-05 11:50:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-01-05 11:50:21 +0100 |
| commit | 1da3072af8182940641bf42316ffaa01cade77b3 (patch) | |
| tree | ad57f68a1656348c9967659d6a1ff85dff2d870b /ide/document.mli | |
| parent | f3e1a1649657424cdd904f512b241defcc39bb2e (diff) | |
Removing GUtil dependency from ide/document.ml.
We reimplement a quick-n-dirty Gtk-free signal handler.
Diffstat (limited to 'ide/document.mli')
| -rw-r--r-- | ide/document.mli | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/ide/document.mli b/ide/document.mli index 8196c0f21..0d803ff00 100644 --- a/ide/document.mli +++ b/ide/document.mli @@ -106,13 +106,10 @@ val print : (** Callbacks on documents *) -class ['a] signals : - 'a GUtil.signal -> - 'a GUtil.signal -> +class type ['a] signals = object - inherit GUtil.ml_signals - method popped : callback:('a -> unit) -> GtkSignal.id - method pushed : callback:('a -> unit) -> GtkSignal.id + method popped : callback:('a -> unit) -> unit + method pushed : callback:('a -> unit) -> unit end val connect : 'a document -> 'a signals |