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 2b849412bbaaa1218620a5948aa1723ac81b151f..22eee2f00ebf0d3c00e601a2dc8e6d04b75cba7d 100644 (file)
--- 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,