From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 22 Nov 2010 12:54:57 +0000 (+0000)
Subject: Small improvement: check now takes the context of the first focused
X-Git-Tag: make_still_working~2688
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9295d7fe073343ef195bcff5453b1cffd30552be;p=helm.git

Small improvement: check now takes the context of the first focused
goal, if any.
---

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 2b849412b..22eee2f00 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -118,9 +118,14 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
       let status = script#grafite_status in
       let _,_,menv,subst,_ = status#obj in
       let ctx = 
-        try let _,(_,ctx,_) = List.hd menv in ctx
-        with Failure "hd" -> []
-      in
+       match Continuationals.Stack.head_goals status#stack with
+          [] -> []
+        | g::tl ->
+           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 m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
           status None ctx menv subst (parsed_text,parsed_text_length,