X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=22eee2f00ebf0d3c00e601a2dc8e6d04b75cba7d;hb=3a5ad4a99fd7f312424200a9241ea1a4ce7fcd29;hp=8e1eb69d481d7d92fa4bf41f62937e3fe8acc787;hpb=098e3728bb1d993145b893b83ac6e01173b58486;p=helm.git

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 8e1eb69d4..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,
@@ -188,7 +193,8 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff
     match statement with
     | `Raw text ->
         if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
-        let ast = MatitaEngine.get_ast grafite_status include_paths text in
+        let strm = Ulexing.from_utf8_string text in
+        let ast = MatitaEngine.get_ast grafite_status include_paths strm in
          ast, text
     | `Ast (st, text) -> st, text
   in