Ideutils: comment on missing Glib utf8 handling function

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16476 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 8 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 1d3088a642..7c4aa3713b 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -59,6 +59,8 @@ let byte_offset_to_char_offset s byte_offset =
   done;
   byte_offset - !extra_bytes
 
+let glib_utf8_pos_to_offset s ~off = byte_offset_to_char_offset s off
+
 let print_id id =
   Minilib.log ("GOT sig id :"^(string_of_int (Obj.magic id)))
 
@@ -404,11 +406,3 @@ let browse_keyword prerr text =
     browse prerr (doc_url() ^ u)
   with Not_found -> prerr ("No documentation found for \""^text^"\".\n")
 
-(* This is missing in lablgtk2.  This one is inefficient, n^2 I guess *)
-let glib_utf8_pos_to_offset s ~off =
-  let n = if Glib.Utf8.validate s then Glib.Utf8.length s else 0 in
-  let rec find i =
-    if i >= n then i
-    else if Glib.Utf8.offset_to_pos s ~pos:0 ~off:i >= off then i
-    else find (i+1)
-  in find 0