aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorletouzey2012-12-07 16:39:48 +0000
committerletouzey2012-12-07 16:39:48 +0000
commit16fd813e55280b9aa95cff788b0099b776a75c74 (patch)
tree440f275ab628a9673d4a65cbc3408140e2a81001
parent2965635533740a4a0fb13a6f0390d56b4321b981 (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.ml26
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)))