]> matita.cs.unibo.it Git - helm.git/commitdiff
Now the time required to eval a command is printed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 26 Oct 2009 13:03:28 +0000 (13:03 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 26 Oct 2009 13:03:28 +0000 (13:03 +0000)
helm/software/matita/matitaScript.ml

index 829806871d1422f435e393faf6044b02cd18a405..3f354ab62a02546572ec0b309c4302102321f2e7 100644 (file)
@@ -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