X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=829806871d1422f435e393faf6044b02cd18a405;hb=a57b60bb92d8587ced8ef5e9e47cdc4daafa40fc;hp=aaa703348af1205c2c70a362a79d09a4c7a9ddf5;hpb=3cb42e0873c101c6c5a8b9967d765b5135882685;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index aaa703348..829806871 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -392,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
@@ -660,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