query generator timing feature improved

[helm.git] / helm / gTopLevel / mQueryGenerator.ml

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 5c6fb27d72ca260e6f931fd7ead3b24421e2d250..bb27633bb5c4694d0cc69f4866cfb4e7b3b5bb32 100644 (file)
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -232,10 +232,16 @@ let call_back f =
    issue := f
 
 let backward e c t level =
+   let t0 = Sys.time () in
    env := e; cont := c;
    let il = inspect t in
    let query = build_inter 0 (il_restrict level il) in
    let query' = restrict_universe query il in
    let query'' = MQList query' in 
-   par () ^ il_out il ^ build_result query''
-
+   let r = build_result query'' in
+   if r <> "" then
+   begin
+      print_endline ("GEN = " ^ string_of_int (List.length il) ^ ":" ^
+         string_of_float (Sys.time () -. t0) ^ "s");
+      par () ^ il_out il ^ r
+   end else ""