X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=2186b75b5ff2d4c9914861031920487d86498197;hb=34cdd4af2d7bdac3bab74a54123fbfcb02fa0403;hp=a67075a29c35f9e55787de387d5cfcf47d92902a;hpb=e950fb06ecbee032b204461475d47be44303bf91;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index a67075a29..2186b75b5 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
@@ -691,7 +691,7 @@ let fresh_script_id =
   let i = ref 0 in
   fun () -> incr i; !i
 
-class script  ~(source_view: GSourceView.source_view)
+class script  ~(source_view: GSourceView2.source_view)
               ~(mathviewer: MatitaTypes.mathViewer) 
               ~set_star
               ~ask_confirmation
@@ -800,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