From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 5 Jul 2005 10:25:19 +0000 (+0000)
Subject: Gtk loop was called only when a proof was terminated. Now it is called after
X-Git-Tag: V_0_7_1~92
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=52f1d65c2f014ae6e45fb1e0b422281c443dc17f;p=helm.git

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 4b548f606..15fe2c9ac 100644
--- 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 = []