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

2 files changed, 6 insertions, 9 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 1d3088a64..7c4aa3713 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
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 56183c520..c22c167ba 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -14,7 +14,11 @@ val cb : GData.clipboard
 val doc_url : unit -> string
 val browse : (string -> unit) -> string -> unit
 val browse_keyword : (string -> unit) -> string -> unit
+
+(* These two functions are equivalent, the latter is named following
+   glib schema, and exists in glib but is not in lablgtk2 *)
 val byte_offset_to_char_offset : string -> int -> int
+val glib_utf8_pos_to_offset : string -> off:int -> int
 
 type timer = { run : ms:int -> callback:(unit->bool) -> unit;
                kill : unit -> unit }
@@ -92,4 +96,3 @@ val io_read_all : Glib.Io.channel -> string
 val run_command :
   (string -> unit) -> (Unix.process_status -> unit) -> string -> unit
 
-val glib_utf8_pos_to_offset : string -> off:int -> int