diff options
| -rw-r--r-- | kernel/names.ml | 5 | ||||
| -rw-r--r-- | kernel/names.mli | 1 | ||||
| -rw-r--r-- | library/nameops.ml | 20 |
3 files changed, 16 insertions, 10 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 1f138581c..831b6ad46 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -50,6 +50,11 @@ struct | None -> true | Some _ -> false + let of_bytes s = + let s = Bytes.to_string s in + check_soft s; + String.hcons s + let of_string s = let () = check_soft s in let s = String.copy s in diff --git a/kernel/names.mli b/kernel/names.mli index 6b0a80625..be9b9422b 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -43,6 +43,7 @@ sig (** Check that a string may be converted to an identifier. @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) + val of_bytes : bytes -> t val of_string : string -> t (** Converts a string into an identifier. @raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters. diff --git a/library/nameops.ml b/library/nameops.ml index 6020db33d..098f5112f 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -61,7 +61,7 @@ let make_ident sa = function if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n) else sa ^ "_" ^ (string_of_int n) in Id.of_string s - | None -> Id.of_string (String.copy sa) + | None -> Id.of_string sa let root_of_id id = let suffixstart = cut_ident true id in @@ -92,20 +92,20 @@ let increment_subscript id = 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 (Char.code c + 1); + let newid = Bytes.of_string id in + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid carrypos (Char.chr (Char.code c + 1)); newid end else begin - let newid = id^"0" in + let newid = Bytes.of_string (id^"0") in if carrypos < len-1 then begin - String.fill newid (carrypos+1) (len-1-carrypos) '0'; - newid.[carrypos+1] <- '1' + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid (carrypos+1) '1' end; newid end - in Id.of_string (add (len-1)) + in Id.of_bytes (add (len-1)) let has_subscript id = let id = Id.to_string id in @@ -113,9 +113,9 @@ let has_subscript id = let forget_subscript id = let numstart = cut_ident false id in - let newid = String.make (numstart+1) '0' in + let newid = Bytes.make (numstart+1) '0' in String.blit (Id.to_string id) 0 newid 0 numstart; - (Id.of_string newid) + (Id.of_bytes newid) let add_suffix id s = Id.of_string (Id.to_string id ^ s) let add_prefix s id = Id.of_string (s ^ Id.to_string id) |