query generator timing feature improved

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 9dd40336a0d1f625df3ebba5d847b425efb87709..bb27633bb5c4694d0cc69f4866cfb4e7b3b5bb32 100644 (file)
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -220,21 +220,8 @@ let locate_query s =
                        )
              )
 
-let locate s =
- (*CSC: the code should be: Mqint.execute (locate_query s)                  *)
- (*CSC: what follows is the patch to map mutual inductive definition blocks *)
- (*CSC: URIs (i.e. no fragment identifier at all) to the URIs of the first  *)
- (*CSC: mutual inductive type of their block.                               *)
- let MQRefs uris = Mqint.execute (locate_query s) in
-  MQRefs
-   (List.map
-    (function uri ->
-      if String.sub uri (String.length uri - 4) 4 = ".con" then uri else
-       uri ^ "#1/1"
-    ) uris)
-;;
-
-let locate_html s = build_result (locate_query s);;
+let locate s = Mqint.execute (locate_query s)
+let locate_html s = build_result (locate_query s)
 
 let levels e c t =
    env := e; cont := c;
@@ -245,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 ""