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 | |
| 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.
| -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) = |