Using ML signalling in CoqIDE

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16322 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 3 deletions

diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli
index 4ddb84f69..4311af99a 100644
--- a/ide/wg_Completion.mli
+++ b/ide/wg_Completion.mli
@@ -8,16 +8,23 @@
 
 module Proposals : sig type t end
 
+class type complete_model_signals =
+  object ('a)
+    method after : 'a
+    method disconnect : GtkSignal.id -> unit
+    method start_completion : callback:(int -> unit) -> GtkSignal.id
+    method update_completion : callback:(int * string * Proposals.t -> unit) -> GtkSignal.id
+    method end_completion : callback:(unit -> unit) -> GtkSignal.id
+  end
+
 class complete_model : Coq.coqtop -> GText.buffer ->
 object
   method active : bool
+  method connect : complete_model_signals
   method set_active : bool -> unit
   method store : GTree.model_filter
   method column : string GTree.column
   method handle_proposal : Gtk.tree_path -> unit
-  method start_completion_callback : (int -> unit) -> unit
-  method update_completion_callback : (int -> string -> Proposals.t -> unit) -> unit
-  method end_completion_callback : (unit -> unit) -> unit
 end
 
 class complete_popup : complete_model -> GText.view ->