From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 14 Apr 2006 10:13:07 +0000 (+0000)
Subject: the same utf8 bug as before
X-Git-Tag: 0.4.95@7852~1505
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9fb1e5c3cab754ada57dab5c2fdac6f4b97d7146;p=helm.git

the same utf8 bug as before
---

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index 7decc583c..e9a84c9b4 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -890,11 +890,12 @@ class gui () =
     method private nextLigature () =
       let iter = source_buffer#get_iter_at_mark `INSERT in
       let write_ligature len s =
+        assert(Glib.Utf8.validate s);
         source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars len);
         source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s
       in
       let get_ligature word =
-        let len = String.length word in
+        let len = MatitaGtkMisc.utf8_string_length word in
         let aux_tex () =
           try
             for i = len - 1 downto 0 do
@@ -933,7 +934,7 @@ class gui () =
           (match CicNotationLexer.lookup_ligatures ligature with
           | [] -> ()
           | hd :: tl ->
-              write_ligature (String.length ligature) hd;
+              write_ligature (MatitaGtkMisc.utf8_string_length ligature) hd;
               next_ligatures <- tl @ [ hd ])
       | hd :: tl ->
           write_ligature 1 hd;