diff options
| -rw-r--r-- | ide/wg_Completion.ml | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index dcb71d96a1..367a897394 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -98,8 +98,12 @@ class completion_provider coqtop = method populate ctx = let iter = ctx#iter in + let () = insert_offset <- iter#offset in + let () = Minilib.log (Printf.sprintf "Completion at offset: %i" insert_offset) in let buffer = new GText.buffer iter#buffer in + if not (Gtk_parsing.ends_word iter#backward_char) then self#add_proposals ctx Proposals.empty else let start = Gtk_parsing.find_word_start iter in + if iter#offset - start#offset < auto_complete_length then self#add_proposals ctx Proposals.empty else let w = start#get_text ~stop:iter in let () = Minilib.log ("Completion of prefix: '" ^ w ^ "'") in let (off, prefix, props) = cache in @@ -127,17 +131,7 @@ class completion_provider coqtop = let occupied () = update synt in Coq.try_grab coqtop query occupied - method matched ctx = - if !active then - let iter = ctx#iter in - let () = insert_offset <- iter#offset in - let log = Printf.sprintf "Completion at offset: %i" insert_offset in - let () = Minilib.log log in - if Gtk_parsing.ends_word iter#backward_char then - let start = Gtk_parsing.find_word_start iter in - iter#offset - start#offset >= auto_complete_length - else false - else false + method matched ctx = !active method activation = [`INTERACTIVE; `USER_REQUESTED] |