From 52f1d65c2f014ae6e45fb1e0b422281c443dc17f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 5 Jul 2005 10:25:19 +0000 Subject: [PATCH] Gtk loop was called only when a proof was terminated. Now it is called after every line. --- helm/matita/matitaScript.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) 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 = [] -- 2.39.5