X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=aaa703348af1205c2c70a362a79d09a4c7a9ddf5;hb=8cb2490b5b202549a596cfd1d0f166a5ee43fc4e;hp=dcddf7b2cc93cad40ef7f9bc63fef764ba2c9aff;hpb=bee436af0c6ceb1c83259c94036df8b12f901f2d;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index dcddf7b2c..aaa703348 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -371,15 +371,23 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
   | TA.Screenshot (_,name) -> 
        let status = script#grafite_status in
        let _,_,menv,subst,_ = status#obj in
-       let sequent = List.hd menv in
-       guistuff.mathviewer#screenshot status sequent menv subst name;
+       let name = Filename.dirname (script#filename) ^ "/" ^ name in
+       let sequents = 
+         let selected = Continuationals.Stack.head_goals status#stack in
+         List.filter (fun x,_ -> List.mem x selected) menv         
+       in
+       guistuff.mathviewer#screenshot status sequents menv subst name;
        [status, parsed_text], "", parsed_text_length
   | TA.NCheck (_,t) ->
       let status = script#grafite_status in
-      let ctx = [] in
+      let _,_,menv,subst,_ = status#obj in
+      let ctx = 
+        try let _,(_,ctx,_) = List.hd menv in ctx
+        with Failure "hd" -> []
+      in
       let m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
-          None status [] [] ctx (parsed_text,parsed_text_length,
+          None status ctx menv subst (parsed_text,parsed_text_length,
             CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne))  
           (* XXX use the metasenv, if possible *)
       in