Use the GTK completion widget in CoqIDE

[ppedrot]

Fixes #9945

• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

[herbelin]

Are there some parts of the code particularly to double-check? Trusting otherwise.

[ppedrot]

@eponier and @Alizter already commented on the bug report about the usability of this patch. Remaining issues that I don't know how to solve:

• The completion pop-up does not have any border (@eponier)
• Picks up words that shouldn't be considered (@Alizter)
• The box appears over the text sometimes (@Alizter)
• When pressing backspace it should go away (@Alizter)

These behaviours are hardwired in GtkSourceView, and we have no control over them AFAICT.

[eponier]

The point about the border is really a minor one.

[ppedrot]

I consider this ready. It could even be eligible for 8.11.0, but I am afraid this is lacking a larger test base.

[ejgallego]

After testing, IMO this looks pretty good.

Even if we need to tweak some stuff, the PR cannot be worse than the current status so I'm going to merge.

[ppedrot]

In the end, I think I am going to backport this in 8.11.0. I'll test it a bit more before, but the answers from our aforementioned guinea pigs and my limited poking with a stick seemed to be supporting this.

[ejgallego]

As discussed on gitter, I also think the backport is a good idea.