From cfe99ef73d9470ec215404d6e1b2fe69cc677cd0 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Tue, 19 Mar 2013 21:07:01 +0000 Subject: Using ML signalling in CoqIDE git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16322 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/wg_Completion.mli | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'ide/wg_Completion.mli') 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 -> -- cgit v1.2.3