patch by Brian committed, cut&paste should not crash matita any longer

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 3cc3b2547a4bf76d63e6d3acb14d96597e3cf0eb..d04fbcadab4b8bcace82958733d197b007742cc4 100644 (file)
--- 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