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 | |
| 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.
| -rw-r--r-- | ide/gtk_parsing.ml | 71 | ||||
| -rw-r--r-- | ide/wg_Completion.ml | 2 |
2 files changed, 34 insertions, 39 deletions
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index a84c161a84..8e6d9f75c7 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -12,50 +12,45 @@ let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0) let prime = Glib.Utf8.to_unichar "'" ~pos:(ref 0) let dot = Glib.Utf8.to_unichar "." ~pos:(ref 0) -(* TODO: avoid num and prime at the head of a word *) -let is_word_char c = - Glib.Unichar.isalnum c || c = underscore || c = prime || c = dot +let find_word_start (it:GText.iter) = + let rec aux it good = + if it#is_start then good + else + let it = it#backward_char in + let c = it#char in + if Glib.Unichar.isalpha c || c = underscore then aux it it + else if Glib.Unichar.isalnum c || c = prime || c = dot then aux it good + else good in + aux it it +let find_word_end (it:GText.iter) = + let rec aux it good = + if it#is_end then good + else + let c = it#char in + let it = it#forward_char in + if Glib.Unichar.isalnum c || c = prime || c = underscore then aux it it + else if c = dot then aux it good + else good in + aux it it let starts_word (it:GText.iter) = - (it#is_start || - (let c = it#backward_char#char in - not (is_word_char c))) + if it#is_start then true + else + let it = it#backward_char in + let c = it#char in + if Glib.Unichar.isalpha c || c = underscore then + it#equal (find_word_start it) + else false let ends_word (it:GText.iter) = - (it#is_end || - let c = it#forward_char#char in - not (is_word_char c) - ) - -let find_word_start (it:GText.iter) = - let rec step_to_start it = - Minilib.log "Find word start"; - if not it#nocopy#backward_char then - (Minilib.log "find_word_start: cannot backward"; it) - else if is_word_char it#char - then step_to_start it - else begin - ignore(it#nocopy#forward_char); - Minilib.log ("Word start at: "^(string_of_int it#offset)); - it - end - in - step_to_start it#copy - -let find_word_end (it:GText.iter) = - let rec step_to_end (it:GText.iter) = - Minilib.log "Find word end"; + if it#is_end then true + else let c = it#char in - if c<>0 && is_word_char c then ( - ignore (it#nocopy#forward_char); - step_to_end it - ) else ( - Minilib.log ("Word end at: "^(string_of_int it#offset)); - it) - in - step_to_end it#copy - + let it = it#forward_char in + if Glib.Unichar.isalnum c || c = prime || c = underscore then + it#equal (find_word_end it) + else false let get_word_around (it:GText.iter) = let start = find_word_start it in diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 98390e810f..ac6712909e 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -175,7 +175,7 @@ object (self) let log = Printf.sprintf "Completion at offset: %i" insert_offset in let () = Minilib.log log in let prefix = - if Gtk_parsing.ends_word iter#backward_char then + if Gtk_parsing.ends_word iter then let start = Gtk_parsing.find_word_start iter in let w = buffer#get_text ~start ~stop:iter () in if String.length w >= auto_complete_length then Some (w, start) |
