X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=3f354ab62a02546572ec0b309c4302102321f2e7;hb=fb2fabf6c94d6a2f930b7a84673c90af32c48803;hp=d4ef4c6e019cdf7d51a6b0ae8c2b59be02b117e9;hpb=ac45365fea68bc3ce11afe76bc7595e53b235777;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index d4ef4c6e0..3f354ab62 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -372,7 +372,11 @@ 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 name = Filename.dirname (script#filename) ^ "/" ^ name in
-       guistuff.mathviewer#screenshot status menv 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
@@ -388,7 +392,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
           (* XXX use the metasenv, if possible *)
       in
       guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
-      [], "", parsed_text_length
+      [status, parsed_text], "", parsed_text_length
 
 let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
   let module MQ = MetadataQuery in
@@ -656,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
@@ -796,12 +800,15 @@ object (self)
    let s = match statement with Some s -> s | None -> self#getFuture in
    if self#bos then LibraryClean.clean_baseuris [self#buri_of_current_file];
    HLog.debug ("evaluating: " ^ first_line s ^ " ...");
+   let time1 = Unix.gettimeofday () in
    let entries, newtext, parsed_len = 
     try
      eval_statement self#include_paths buffer guistuff
       self#grafite_status userGoal self (`Raw s)
     with End_of_file -> raise Margin
    in
+   let time2 = Unix.gettimeofday () in
+   HLog.debug ("... done in " ^ string_of_float (time2 -. time1) ^ "s");
    let new_statuses, new_statements =
      let statuses, texts = List.split entries in
      statuses, texts