From 5cd629439dd0398db27e6fcb3e3766a361cc5d51 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 20 Jan 2006 12:20:30 +0000 Subject: [PATCH] bugfix: when looking for a goal from the continuationals stack handle the case that no one is there (i.e. the proof is completed) avoiding run-away exceptions --- helm/matita/matitaScript.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 4b1b994d9..188726d95 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -509,7 +509,9 @@ object (self) bottom) and we will face a macro *) match self#grafite_status.proof_status with Incomplete_proof p -> - userGoal <- Some (Continuationals.Stack.find_goal p.stack) + userGoal <- + (try Some (Continuationals.Stack.find_goal p.stack) + with Failure _ -> None) | _ -> userGoal <- None method private _retract offset lexicon_status grafite_status new_statements -- 2.39.2