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