aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGuillaume Melquiond2019-11-07 16:27:16 +0100
committerGuillaume Melquiond2019-11-07 16:27:16 +0100
commit5b8a2855f719f42d81dd9ac3e8c5737fa8c7b2db (patch)
treead1580a3cc20413b78f68f11c49eb0748eb73d39
parent5c5831e35747f25d8aeadf10a13cd60e9b7adfbb (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.ml71
-rw-r--r--ide/wg_Completion.ml2
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)