aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-28 18:48:48 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-28 18:48:48 +0000
commitbde6c473017c5ee4cd6d20b2d8aa9f3c56930c57 (patch)
treece6030475bcd176242e14c7bf2a9830cb9cc293a /ide/coqide.ml
parent9e2cfa798fc4fb0d50433f14eb714d8f90a82b88 (diff)
Suite commit 9256: autres cas incorrects de prise en compte de @ dans les ident
pour F4 dans CoqIDE git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9307 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml5
1 files changed, 2 insertions, 3 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 908c1b798..a303ec6c4 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -328,7 +328,6 @@ let remove_current_view_page () =
kill_input_view c;
((notebook ())#get_nth_page c)#misc#hide ()
-
let is_word_char c =
(* TODO: avoid num and prime at the head of a word *)
Glib.Unichar.isalnum c || c = underscore || c = prime
@@ -342,14 +341,14 @@ let starts_word it =
let ends_word it =
(not it#copy#nocopy#forward_char ||
let c = it#forward_char#char in
- not (Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase)
+ not (is_word_char c)
)
let inside_word it =
let c = it#char in
not (starts_word it) &&
not (ends_word it) &&
- (Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase)
+ is_word_char c
let is_on_word_limit it = inside_word it || ends_word it