From 2765b4ab727995efeebb972973d6032b06095845 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 12 Dec 2005 16:20:26 +0000 Subject: [PATCH] bugfix: tactic invocations from contextual menu no longer generate content out of sync wrt locked mark --- helm/matita/matitaMathView.ml | 2 +- helm/matita/matitaScript.ml | 11 +++++------ 2 files changed, 6 insertions(+), 7 deletions(-) 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 *) -- 2.39.2