From 7d614710615f15035ae6750babbf37b0ce7206d7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 8 Apr 2020 19:04:49 +0200
Subject: Coqide completion: Avoiding using an iterator in an apparently
 sensitive code.

Let's see if it fixes #11943. See there for explanations about the
related segfault.
---
 ide/wg_Completion.ml | 16 +++++-----------
 1 file 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]
 
-- 
cgit v1.2.3


From bf0c1214c9d0e46c4188fd7471c47aa330755e69 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 Apr 2020 12:13:38 +0200
Subject: Change log for #12068 (Coqide segfault tentative fix).

---
 .../09-coqide/12068-master+coqide-completion-no-matched.rst          | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/09-coqide/12068-master+coqide-completion-no-matched.rst

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>`_).
-- 
cgit v1.2.3


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(-)

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