coqide: corrections pour utf8 de coq. highlight synchrone=repare le bug autorepeat des paste. configuration des accel rateurs. les chaines peuvent contenir des points. Bug: les phrases ne peuvent pas contenir .\sep. Or c'est permis par les Notation.

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

1 files changed, 17 insertions, 9 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 20a06ae12e..6373e5a344 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -10,14 +10,22 @@ let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
 let is_char_start c = let code = Char.code c in code < 0x80 || code >= 0xc0
 
 let byte_offset_to_char_offset s byte_offset = 
-  assert (byte_offset < String.length s);
-  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
-
+  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 process_pending () =
   while Glib.Main.pending () do 
@@ -50,7 +58,7 @@ let try_export file_name s =
       if (fst (Glib.Convert.get_charset ())) then
 	s 
       else
-	Glib.Convert.locale_from_utf8 s 
+	(try Glib.Convert.locale_from_utf8 s with _ -> prerr_endline "Warning: exporting to utf8";s)
     in
     let oc = open_out file_name in
     output_string oc s;