From bf07cdb635f9a3eb858a1b7980f848f3e40a439c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 8 Jul 2005 09:59:02 +0000 Subject: [PATCH] it seems the sequent window is refreshed properly now --- helm/matita/matitaScript.ml | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 63a6ed007..ce613ef71 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -396,13 +396,17 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; try self#_advance ?statement (); self#notify - with Margin -> self#notify + with + | Margin -> self#notify + | exc -> self#notify; raise exc method retract () = try self#_retract (); self#notify - with Margin -> self#notify + with + | Margin -> self#notify + | exc -> self#notify; raise exc method private getFuture = buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark)) @@ -499,7 +503,9 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; in dowhile (getpos ()); self#notify - with Margin -> self#notify) + with + | Margin -> self#notify + | exc -> self#notify; raise exc) | `Cursor -> let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in let cursor_iter () = buffer#get_iter_at_mark `INSERT in @@ -521,8 +527,10 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; (back_until_cursor (); self#notify) else (* cursor = locked *) () - with Margin -> self#notify) - + with + | Margin -> self#notify + | exc -> self#notify; raise exc) + method onGoingProof () = match self#status.proof_status with | No_proof | Proof _ -> false -- 2.39.2