Better handling of asynchronous completion.

1 files changed, 3 insertions, 1 deletions

diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index 21d794ce6e..396939cfcc 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -109,9 +109,11 @@ class completion_provider coqtop =
         let props = self#update_proposals w in
         self#add_proposals ctx props
       else
+        let cancel = ref false in
+        let _ = ctx#connect#cancelled ~callback:(fun () -> cancel := true) in
         let update props =
           let () = cache <- (start_offset, w, props) in
-          self#add_proposals ctx props;
+          if not !cancel then self#add_proposals ctx props
         in
         (* If not in the cache, we recompute it: first syntactic *)
         let synt = get_syntactic_completion buffer w Proposals.empty in