From b011869c7c9d18aad8ccd4d1ced0b6c36e472863 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 25 Jan 2013 18:57:18 +0000 Subject: Fixing autocompletion in CoqIDE git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16145 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/wg_ScriptView.ml | 98 ++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 73 insertions(+), 25 deletions(-) (limited to 'ide/wg_ScriptView.ml') diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 0ce09453c..4484dc4d8 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -10,13 +10,37 @@ open Ideutils open GText open Gtk_parsing +type insert_action = { + ins_val : string; + ins_off : int; + ins_len : int; +} + +type delete_action = { + del_val : string; + del_off : int; + del_len : int; +} + type action = - | Insert of string * int * int (* content*pos*length *) - | Delete of string * int * int (* content*pos*length *) + | Insert of insert_action + | Delete of delete_action let neg act = match act with - | Insert (s,i,l) -> Delete (s,i,l) - | Delete (s,i,l) -> Insert (s,i,l) + | Insert act -> + let act = { + del_len = act.ins_len; + del_off = act.ins_off; + del_val = act.ins_val; + } in + Delete act + | Delete act -> + let act = { + ins_len = act.del_len; + ins_off = act.del_off; + ins_val = act.del_val; + } in + Insert act type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj @@ -87,6 +111,8 @@ object (self) val mutable last_completion = (-1, "", Proposals.empty) (* this variable prevents CoqIDE from autocompleting when we have deleted something *) val mutable is_auto_completing = false + (* this mutex ensure that CoqIDE will not try to autocomplete twice *) + val mutable lock_auto_completing = true method auto_complete = auto_complete @@ -95,10 +121,12 @@ object (self) method private dump_debug () = let iter = function - | Insert (s, p, l) -> - Printf.eprintf "Insert of '%s' at %d (length %d)\n" s p l - | Delete (s, p, l) -> - Printf.eprintf "Delete '%s' from %d (length %d)\n" s p l + | Insert act -> + Printf.eprintf "Insert of '%s' at %d (length %d)\n" + act.ins_val act.ins_off act.ins_len + | Delete act -> + Printf.eprintf "Delete '%s' from %d (length %d)\n" + act.del_val act.del_off act.del_len in if false (* !debug *) then begin Minilib.log "==========Undo Stack top============="; @@ -135,13 +163,13 @@ object (self) method private process_action = function | [] -> false - | Insert (s, p, l) :: history -> - let start = self#buffer#get_iter_at_char p in - let stop = start#forward_chars l in + | Insert ins :: history -> + let start = self#buffer#get_iter (`OFFSET ins.ins_off) in + let stop = start#forward_chars ins.ins_len in self#buffer#delete_interactive ~start ~stop () - | Delete (s, p, l) :: history -> - let iter = self#buffer#get_iter_at_char p in - self#buffer#insert_interactive ~iter s + | Delete del :: history -> + let iter = self#buffer#get_iter (`OFFSET del.del_off) in + self#buffer#insert_interactive ~iter del.del_val method undo () = Minilib.log "UNDO"; @@ -155,21 +183,32 @@ object (self) method private handle_insert iter s = (* we're inserting, so we may autocomplete *) - is_auto_completing <- true; + is_auto_completing <- true + + method private handle_after_insert iter s = (* Save the insert action *) - let action = Insert (s, iter#offset, Glib.Utf8.length s) in + let ins = { + ins_val = s; + ins_off = iter#offset; + ins_len = Glib.Utf8.length s; + } in + let action = Insert ins in history <- action :: history; redo <- []; self#dump_debug () method private handle_delete ~start ~stop = (* disable autocomplete *) - is_auto_completing <- false; + is_auto_completing <- false + + method private handle_after_delete ~start ~stop = (* Save the delete action *) - let start_offset = start#offset in - let stop_offset = stop#offset in - let s = self#buffer#get_text ~start ~stop () in - let action = Delete (s, start_offset, stop_offset - start_offset) in + let del = { + del_val = self#buffer#get_text ~start ~stop (); + del_off = start#offset; + del_len = stop#offset - start#offset; + } in + let action = Delete del in history <- action :: history; redo <- []; self#dump_debug (); @@ -198,11 +237,14 @@ object (self) let len2 = String.length w in String.sub proposal len2 (len1 - len2) in + self#buffer#begin_user_action (); ignore (self#buffer#delete_selection ()); - ignore (self#buffer#insert_interactive suffix); + let iter = self#buffer#get_iter (`OFFSET cur_offset) in + ignore (self#buffer#insert_interactive ~iter suffix); let ins = self#buffer#get_iter (`OFFSET cur_offset) in let sel = self#buffer#get_iter `INSERT in - self#buffer#select_range sel ins + self#buffer#select_range sel ins; + self#buffer#end_user_action (); end; k () in @@ -217,7 +259,11 @@ object (self) end method private may_auto_complete () = - if auto_complete && is_auto_completing then self#do_auto_complete () + if auto_complete && is_auto_completing && lock_auto_completing then begin + lock_auto_completing <- false; + self#do_auto_complete (); + lock_auto_completing <- true; + end (* HACK: missing gtksourceview features *) method right_margin_position = @@ -324,9 +370,11 @@ object (self) initializer (* Install undo managing *) + ignore (self#buffer#connect#after#insert_text ~callback:self#handle_after_insert); + ignore (self#buffer#connect#after#delete_range ~callback:self#handle_after_delete); + (* Install auto-completion *) ignore (self#buffer#connect#insert_text ~callback:self#handle_insert); ignore (self#buffer#connect#delete_range ~callback:self#handle_delete); - (* Install auto-completion *) ignore (self#buffer#connect#after#end_user_action ~callback:self#may_auto_complete); (* HACK: Redirect the undo/redo signals of the underlying GtkSourceView *) ignore (self#connect#undo -- cgit v1.2.3