From 9295d7fe073343ef195bcff5453b1cffd30552be Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 22 Nov 2010 12:54:57 +0000
Subject: [PATCH] Small improvement: check now takes the context of the first
 focused goal, if any.

---
 matita/matita/matitaScript.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

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