diff options
| author | Pierre-Marie Pédrot | 2019-05-07 12:57:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-07 12:57:18 +0200 |
| commit | 8aa64e7c4661549fef63a1c9c2e4e5284db911d8 (patch) | |
| tree | 39253cd97b57675765cff0374224742d58363741 | |
| parent | 45dcc1248cd2bdf00a2bcead69d6b2ed78afc51d (diff) | |
| parent | 62b19246a81adbd07992cca91009faf012c5e9dd (diff) | |
Merge PR #10063: CoqIDE: recognize qualified identifiers as words.
Reviewed-by: ppedrot
| -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) = |