added mark moving refresh

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 94cedf29b748e1419d83d14a7486a79b8838ba0c..4b548f6069f7e43860bf21125f2cb859ee14ef3e 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -422,7 +422,8 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     buffer#move_mark `INSERT old_insert;
     match self#status.proof_status with
        Incomplete_proof (_,goal) -> self#setGoal goal
-     | _ -> ()
+     | _ -> ();
+    while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
 
   val mutable observers = []