diff options
| author | Jasper Hugunin | 2019-05-03 23:22:56 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2019-05-03 23:22:56 -0700 |
| commit | 62b19246a81adbd07992cca91009faf012c5e9dd (patch) | |
| tree | 6eb12d5ec104e777cdcace6c7ed8f7bdc0d9fdd1 /ide | |
| parent | 6960da4736186fa6214854329f36f558e7aa4d0b (diff) | |
CoqIDE: recognize qualified identifiers as words.
Fixes coq/coq#10062.
The implementation is rough, and does not deal with leading,
trailing, or doubled periods, but the same can be said of the current
handling of leading numbers or primes.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/gtk_parsing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index d554bebdd3..82a5e9cdf6 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -10,11 +10,11 @@ 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 + Glib.Unichar.isalnum c || c = underscore || c = prime || c = dot let starts_word (it:GText.iter) = |