From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 12 Dec 2005 16:20:26 +0000 (+0000)
Subject: bugfix: tactic invocations from contextual menu no longer generate content out of... 
X-Git-Tag: make_still_working~8010
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2765b4ab727995efeebb972973d6032b06095845;hp=99b249b23524cda2d91602ee088fef1a7be253ee;p=helm.git

bugfix: tactic invocations from contextual menu no longer generate content out of sync wrt locked mark
---

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index a7299879a..93adb1c90 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -245,12 +245,12 @@ object (self)
       let pat = self#tactic_text_pattern_of_selection in
       let statement =
         let loc = DisambiguateTypes.dummy_floc in
+        "\n" ^
         GrafiteAstPp.pp_executable ~term_pp:(fun s -> s)
           ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
           (GrafiteAst.Tactical (loc,
             GrafiteAst.Tactic (loc, GrafiteAst.Reduce (loc, kind, pat)),
             Some (GrafiteAst.Semicolon loc))) in
-      HLog.debug ("soon I'll evaluate: " ^ statement);
       (MatitaScript.current ())#advance ~statement () in
     connect_menu_item copy gui#copy;
     connect_menu_item normalize (reduction_action `Normalize);
diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index a545b65d4..c8411d5cf 100644
--- 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 *)