diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/wg_Completion.ml | 4 |
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 |