diff options
| author | Guillaume Melquiond | 2019-11-07 16:27:16 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2019-11-07 16:27:16 +0100 |
| commit | 5b8a2855f719f42d81dd9ac3e8c5737fa8c7b2db (patch) | |
| tree | ad1580a3cc20413b78f68f11c49eb0748eb73d39 /kernel | |
| parent | 5c5831e35747f25d8aeadf10a13cd60e9b7adfbb (diff) | |
Do not include final stops in queries. (Fixes #11058)
The bug was introduced by #10063, which eagerly added dots to identifier
without considering whether they are related to the identifier. Along the
way, this commit also prevents primes and digits from being added as
initial characters of identifiers. This works for both word selection and
queries.
Note that there is still a small issue with word selection, when the
current word starts with a digit. Indeed, when double-clicking, GTK will
already have extended the selection to it, so we have no way of preventing
the digit from being part of the selection.
This commit also fixes the unusual calling convention of
Gtk_parsing.end_words.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions
