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 = []