aboutsummaryrefslogtreecommitdiff
path: root/ide/wg_Completion.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/wg_Completion.ml')
-rw-r--r--ide/wg_Completion.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index 367a897394..cc24e71386 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -69,7 +69,7 @@ let is_substring s1 s2 =
if !break then len2 - len1
else -1
-class completion_provider coqtop =
+class completion_provider buffer coqtop =
let self_provider = ref None in
let active = ref true in
let provider = object (self)
@@ -97,7 +97,7 @@ class completion_provider coqtop =
ctx#add_proposals (Option.get !self_provider) props true
method populate ctx =
- let iter = ctx#iter in
+ let iter = buffer#get_iter_at_mark `INSERT 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