From fc2bd56377205f9cc3ff52dd335fd338670fe13b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Apr 2020 15:55:52 +0200
Subject: CoqIDE completion: Relying on INSERT mark of the buffer.

The iterator of the completion context does not seem trustable.
---
 ide/wg_Completion.ml  | 4 ++--
 ide/wg_Completion.mli | 2 +-
 ide/wg_ScriptView.ml  | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'ide')

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
diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli
index 93c4cbb602..8bb34fbbca 100644
--- a/ide/wg_Completion.mli
+++ b/ide/wg_Completion.mli
@@ -10,7 +10,7 @@
 
 module Proposals : sig type t end
 
-class completion_provider : Coq.coqtop ->
+class completion_provider : GText.buffer -> Coq.coqtop ->
 object
   inherit GSourceView3.source_completion_provider
   method active : bool
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index f2d9f33d7d..62d58a5f23 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -287,7 +287,7 @@ end
 class script_view (tv : source_view) (ct : Coq.coqtop) =
 
 let view = new GSourceView3.source_view (Gobject.unsafe_cast tv) in
-let provider = new Wg_Completion.completion_provider ct in
+let provider = new Wg_Completion.completion_provider view#buffer ct in
 
 object (self)
   inherit GSourceView3.source_view (Gobject.unsafe_cast tv)
-- 
cgit v1.2.3