aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-21 17:04:22 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-21 17:04:22 +0000
commit76697fb3fd73564c06f7fee23e9a92c8f9da7664 (patch)
tree5bca5db6d607fc006a11d2f4685c4474eaf5e95e /ide/coqide.ml
parent689463a50a4b1da3fd3fcd899146365ca5d1c9a0 (diff)
Pas d'@ dans les identificateurs (pour F4 and co)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9256 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 0b5daaffb..343096f5b 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -329,9 +329,10 @@ let remove_current_view_page () =
((notebook ())#get_nth_page c)#misc#hide ()
-let is_word_char c =
- Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase
-
+let is_word_char c =
+ (* TODO: avoid num and prime at the head of a word *)
+ Glib.Unichar.isalnum c || c = underscore || c = prime
+
let starts_word it =
prerr_endline ("Starts word ? '"^(Glib.Utf8.from_unichar it#char)^"'");
(not it#copy#nocopy#backward_char ||