diff options
| -rw-r--r-- | doc/changelog/09-coqide/12068-master+coqide-completion-no-matched.rst | 5 | ||||
| -rw-r--r-- | ide/wg_Completion.ml | 20 | ||||
| -rw-r--r-- | ide/wg_Completion.mli | 2 | ||||
| -rw-r--r-- | ide/wg_ScriptView.ml | 2 |
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) |