X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=93adb1c90fc529356bb4db6457aaf96fa1d24357;hb=de21be5819bd35a2cb83b3d33b1c578d970a32c7;hp=a7299879a3a3292ab31785e0e7a558a74a4599c1;hpb=99b249b23524cda2d91602ee088fef1a7be253ee;p=helm.git 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);