From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 5 Jul 2005 10:05:33 +0000 (+0000)
Subject: added mark moving refresh
X-Git-Tag: V_0_7_1~95
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bf299c70cb9ff4e73f1a31156e4e7a19221859d7;p=helm.git

added mark moving refresh
---

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 94cedf29b..4b548f606 100644
--- 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 = []