From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 20 Jan 2006 12:20:30 +0000 (+0000)
Subject: bugfix: when looking for a goal from the continuationals stack handle the case that... 
X-Git-Tag: make_still_working~7797
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5cd629439dd0398db27e6fcb3e3766a361cc5d51;p=helm.git

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
---

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