From 943cb0b91cfb15e2bdc04c626035e8cba0e65c02 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 25 Apr 2013 14:14:36 +0000 Subject: lablgtk2 misses Glib.Utf8.pos_to_offset, workaround in ideutils git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16455 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/ideutils.ml | 9 +++++++++ ide/ideutils.mli | 2 ++ 2 files changed, 11 insertions(+) (limited to 'ide') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 1464181f4..1d3088a64 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -403,3 +403,12 @@ let browse_keyword prerr text = let u = Lazy.force url_for_keyword text in 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 cc34a355a..56183c520 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -91,3 +91,5 @@ 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 -- cgit v1.2.3