From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 17 Apr 2013 10:50:45 +0000 (+0000)
Subject: Fixes a bug which caused Meta_not_found exceptions to be raised after qed-ing a
X-Git-Tag: make_still_working~1188
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f811e07f481b135bd7c621c2d10a268dc35d599b;p=helm.git

Fixes a bug which caused Meta_not_found exceptions to be raised after qed-ing a
lemma with unskipped goals closed by side-effect.
---

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 54850f112..5086eb845 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -663,6 +663,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
             | _ -> status)
          else
           status in
+        (* purge tinycals stack *)
+        let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
+        let status = status#set_stack ninitial_stack in
 (*
 	  try 
 	    index_eq uri status
diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index d86871963..6a03e3538 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -117,8 +117,13 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
            if tl <> [] then
             HLog.warn
              "Many goals focused. Using the context of the first one\n";
-           let _, ctx, _ = NCicUtils.lookup_meta g menv in
-            ctx in
+           let ctx = try
+             let _, ctx, _ = NCicUtils.lookup_meta g menv in ctx
+             with NCicUtils.Meta_not_found _ -> 
+               HLog.warn "Current goal is closed. Using empty context.";
+               [ ]
+           in ctx
+      in
       let m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
           status `XTNone ctx menv subst (parsed_text,parsed_text_length,