Merge PR #12068: Coqide completion: tentative fix for #11943

Reviewed-by: ppedrot

4 files changed, 14 insertions, 15 deletions

diff --git a/doc/changelog/09-coqide/12068-master+coqide-completion-no-matched.rst b/doc/changelog/09-coqide/12068-master+coqide-completion-no-matched.rst
new file mode 100644
index 0000000000..dbb4bdecab
--- /dev/null
+++ b/doc/changelog/09-coqide/12068-master+coqide-completion-no-matched.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  New patch presumably fixing the random Coq 8.11 segfault issue with CoqIDE completion
+  (`#12068 <https://github.com/coq/coq/pull/12068>`_,
+  by Hugo Herbelin, presumably fixing
+  `#11943 <https://github.com/coq/coq/pull/11943>`_).
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index dcb71d96a1..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,9 +97,13 @@ 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
+      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]
 
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)