X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=829806871d1422f435e393faf6044b02cd18a405;hb=667640d70feb01f2a800b548fa019c92b103d75a;hp=9874e71840179f20ebe4dec9020ebe105a718a04;hpb=cf4a3f9226194e0f6dc9572dea1090e2bfa55219;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 9874e7184..829806871 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -368,17 +368,31 @@ let cic2grafite context menv t =
 let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
   let parsed_text_length = String.length parsed_text in
   match mac with
+  | TA.Screenshot (_,name) -> 
+       let status = script#grafite_status in
+       let _,_,menv,subst,_ = status#obj in
+       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
       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
@@ -641,6 +655,15 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff
       let parsed_text, _, _, parsed_text_length = text_of_loc loc in
        [grafite_status,parsed_text],"",
         parsed_text_length
+  | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
+     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
+  | GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))) 
+    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
   | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> 
       let parsed_text, _, _, parsed_text_length = text_of_loc loc in
       let remain_len = String.length unparsed_text - parsed_text_length in
@@ -663,12 +686,6 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff
       | (statuses,text)::tl ->
          (statuses,parsed_text ^ text)::tl,"",parsed_text_length + len
       | [] -> [], "", 0)
-  | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
-     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
   
 let fresh_script_id =
   let i = ref 0 in