Now the time required to eval a command is printed.

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 829806871d1422f435e393faf6044b02cd18a405..3f354ab62a02546572ec0b309c4302102321f2e7 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -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 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 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
    let new_statuses, new_statements =
      let statuses, texts = List.split entries in
      statuses, texts