X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=a67075a29c35f9e55787de387d5cfcf47d92902a;hb=7288b45eacf9f7dcd118b3b89b81ff19ae9d6ce5;hp=e191ee7b31d6c09a01795c2b824297c0dfb534e3;hpb=590b41b39d52ae1e320bf1c01220b06fadb1ba8d;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index e191ee7b3..a67075a29 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -371,9 +371,12 @@ 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
        let name = Filename.dirname (script#filename) ^ "/" ^ name in
-       guistuff.mathviewer#screenshot status sequent menv subst name;
+       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
@@ -657,7 +660,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff
       eval_executable include_paths buffer guistuff 
        grafite_status user_goal unparsed_text skipped nonskipped script ex loc
   | GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))) 
-    (*when Helm_registry.get_bool "matita.literate" *) ->
+    when Helm_registry.get_bool "matita.execcomments" ->
      let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
       eval_executable include_paths buffer guistuff 
        grafite_status user_goal unparsed_text skipped nonskipped script ex loc