From a7e36d2d1da42fb17a2a6c1c737bddc90b2d3040 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 26 Oct 2009 13:03:28 +0000 Subject: [PATCH] Now the time required to eval a command is printed. --- helm/software/matita/matitaScript.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 829806871..3f354ab62 100644 --- 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 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 -- 2.39.2