bugfix: tactic invocations from contextual menu no longer generate content out of...

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index a545b65d492cb4b65fc0cfaba8985a06ceeb3900..c8411d5cf4e0d5b40d45492bf6e5cfb627af02cd 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -507,15 +507,14 @@ object (self)
       let start = buffer#get_iter_at_mark (`MARK locked_mark) in
       let new_text = String.concat "" new_statements in
       if statement <> None then
-       buffer#insert ~iter:start new_text
-      else
+        buffer#insert ~iter:start new_text
+      else begin
         let s = match st with `Raw s | `Ast (_, s) -> s in
-        if new_text <> String.sub s 0 parsed_len then
-        begin
-          let stop = start#copy#forward_chars parsed_len in
-          buffer#delete ~start ~stop;
+        if new_text <> String.sub s 0 parsed_len then begin
+          buffer#delete ~start ~stop:(start#copy#forward_chars parsed_len);
           buffer#insert ~iter:start new_text;
         end;
+      end;
       self#moveMark (String.length new_text);
       (*
       (match List.rev new_asts with (* advance again on punctuation *)