X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=d04fbcadab4b8bcace82958733d197b007742cc4;hb=2f19651bcec24abfb1bf15ff7e1387daad1f6638;hp=3cc3b2547a4bf76d63e6d3acb14d96597e3cf0eb;hpb=ef98db5ff416ef53004e57cc054e28abd1bf871e;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 3cc3b2547..d04fbcada 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -1132,12 +1132,11 @@ class gui () =
        let inplaceof, symb = Virtuals.symbol_of_virtual last_word in
        self#reset_similarsymbols;
        let s = Glib.Utf8.from_unichar symb in
-       let iter = source_buffer#get_iter_at_mark `INSERT in
        assert(Glib.Utf8.validate s);
        source_buffer#delete ~start:iter 
          ~stop:(iter#copy#backward_chars
            (MatitaGtkMisc.utf8_string_length inplaceof + len));
-       source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) 
+       source_buffer#insert ~iter
          (if inplaceof.[0] = '\\' then s else (s ^ tok));
        true
       with Virtuals.Not_a_virtual -> false