X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=e9a84c9b475179cd4b588388a511bda3959ebddb;hb=a89868740968d139dd4e1d621663bcd4d69d0265;hp=7decc583c58ab4b8de1b7a0dab4b49867792bae9;hpb=07a798607400b0ae70871b201592ae6286118cdb;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 7decc583c..e9a84c9b4 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/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;