Gtk loop was called only when a proof was terminated. Now it is called after

every line.

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 4b548f6069f7e43860bf21125f2cb859ee14ef3e..15fe2c9ac044613ce59f3a432529161fb5c59141 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -420,9 +420,11 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     buffer#move_mark mark ~where:new_mark_pos;
     buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos;
     buffer#move_mark `INSERT old_insert;
-    match self#status.proof_status with
-       Incomplete_proof (_,goal) -> self#setGoal goal
-     | _ -> ();
+    begin
+     match self#status.proof_status with
+        Incomplete_proof (_,goal) -> self#setGoal goal
+      | _ -> ()
+    end ;
     while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
 
   val mutable observers = []