diff options
author | 2001-01-31 11:24:15 +0000 | |
---|---|---|
committer | 2001-01-31 11:24:15 +0000 | |
commit | 7de3189d5f82e11a8f584dd1a6104c7863dcc2b4 (patch) | |
tree | 67bee4f7a715207a1e2a5831588e6e8c3c1744fb /kernel | |
parent | ece4c4c205acf42f07f62c314b0f647fd12367e5 (diff) |
Ajout d'espace dans les règles d'affichage des infix si des lettres figurent dans le token
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1297 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/names.ml | 24 |
1 files changed, 7 insertions, 17 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index fa95bc203..8b1cb71a1 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -6,30 +6,20 @@ open Util (* Utilities *) -let is_letter c = - (c >= Char.code 'a' && c <= Char.code 'z') or - (c >= Char.code 'A' && c <= Char.code 'Z') or - (c >= Char.code '\248' && c <= Char.code '\255') or - (c >= Char.code '\192' && c <= Char.code '\214') or - (c >= Char.code '\216' && c <= Char.code '\246') - let code_of_0 = Char.code '0' let code_of_9 = Char.code '9' -let is_digit c = (c >= code_of_0 && c <= code_of_9) - - (* This checks that a string is acceptable as an ident, i.e. starts with a letter and contains only letters, digits or "'" *) let check_ident s = let l = String.length s in if l = 0 then error "The empty string is not an identifier"; - let c = Char.code (String.get s 0) in + let c = String.get s 0 in if not (is_letter c) then error "An identifier starts with a letter"; for i=1 to l-1 do - let c = Char.code (String.get s i) in - if not (is_letter c or is_digit c or c = Char.code '\'') then + let c = String.get s i in + if not (is_letter c or is_digit c or c = '\'') then error ("Character "^(String.sub s i 1)^" is not allowed in an identifier") done @@ -153,16 +143,16 @@ let id_ord = Pervasives.compare let lift_ident id = let len = String.length id in let rec add carrypos = - let c = Char.code (id.[carrypos]) in + let c = id.[carrypos] in if is_digit c then - if c = code_of_9 then begin + if c = '9' then begin assert (carrypos>0); add (carrypos-1) end else begin let newid = String.copy id in String.fill newid (carrypos+1) (len-1-carrypos) '0'; - newid.[carrypos] <- Char.chr (c + 1); + newid.[carrypos] <- Char.chr (Char.code c + 1); newid end else begin @@ -175,7 +165,7 @@ let lift_ident id = end in add (len-1) -let has_index id = is_digit (Char.code (id.[String.length id - 1])) +let has_index id = is_digit (id.[String.length id - 1]) let restart_ident id = let len = String.length id in |