Fixing annoying autocompletion when deleting text.

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

1 files changed, 9 insertions, 1 deletions

diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 2dae029ee..9bcdc7a3b 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -80,6 +80,8 @@ object (self)
   val mutable auto_complete = false
   val mutable auto_complete_length = 3
   val mutable last_completion = (-1, "", Proposals.empty)
+  (* this variable prevents CoqIDE from autocompleting when we have deleted something *)
+  val mutable is_auto_completing = false
 
   val undo_lock = Mutex.create ()
 
@@ -155,6 +157,9 @@ object (self)
       (Minilib.log "REDO DISCARDED"; true)
 
   method private handle_insert iter s =
+    (* we're inserting, so we may autocomplete *)
+    is_auto_completing <- true;
+    (* Save the insert action *)
     if Mutex.try_lock undo_lock then begin
       let action = Insert (s, iter#offset, Glib.Utf8.length s) in
       history <- action :: history;
@@ -164,6 +169,9 @@ object (self)
     end
 
   method private handle_delete ~start ~stop =
+    (* disable autocomplete *)
+    is_auto_completing <- false;
+    (* Save the delete action *)
     if Mutex.try_lock undo_lock then begin
       let start_offset = start#offset in
       let stop_offset = stop#offset in
@@ -215,7 +223,7 @@ object (self)
     end
 
   method private may_auto_complete () =
-    if auto_complete then self#do_auto_complete ()
+    if auto_complete && is_auto_completing then self#do_auto_complete ()
 
   initializer
     (* Install undo managing *)