From fb6ff8d806fa9e4db3a5cb84163dc7ce3882b578 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 23 Sep 2010 19:55:43 +0000
Subject: [PATCH] patch by Brian committed, cut&paste should not crash matita
 any longer

---
 helm/software/matita/matitaGui.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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
-- 
2.39.2