diff options
| author | letouzey | 2012-12-07 16:39:48 +0000 |
|---|---|---|
| committer | letouzey | 2012-12-07 16:39:48 +0000 |
| commit | 16fd813e55280b9aa95cff788b0099b776a75c74 (patch) | |
| tree | 440f275ab628a9673d4a65cbc3408140e2a81001 | |
| parent | 2965635533740a4a0fb13a6f0390d56b4321b981 (diff) | |
Ideutils: simpler conversion from byte offset to utf8 char offset
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16042 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | ide/ideutils.ml | 26 |
1 files changed, 10 insertions, 16 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index c376df99bc..e5d5ebaa88 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -29,23 +29,17 @@ let set_location = ref (function s -> failwith "not ready") let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT +(** A utf8 char is either a single byte (ascii char, 0xxxxxxx) + or multi-byte (with a leading byte 11xxxxxx and extra bytes 10xxxxxx) *) + +let is_extra_byte c = ((Char.code c) lsr 6 = 2) + let byte_offset_to_char_offset s byte_offset = - if (byte_offset < String.length s) then begin - let count_delta = ref 0 in - for i = 0 to byte_offset do - let code = Char.code s.[i] in - if code >= 0x80 && code < 0xc0 then incr count_delta - done; - byte_offset - !count_delta - end - else begin - let count_delta = ref 0 in - for i = 0 to String.length s - 1 do - let code = Char.code s.[i] in - if code >= 0x80 && code < 0xc0 then incr count_delta - done; - byte_offset - !count_delta - end + let extra_bytes = ref 0 in + for i = 0 to min byte_offset (String.length s - 1) do + if is_extra_byte s.[i] then incr extra_bytes + done; + byte_offset - !extra_bytes let print_id id = Minilib.log ("GOT sig id :"^(string_of_int (Obj.magic id))) |
