From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 13 Sep 2002 14:58:49 +0000 (+0000)
Subject: query generator timing feature improved
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~75
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=65828a2a9173bcdf3bf8f9100d0b9cd01109da94;p=helm.git

query generator timing feature improved
---

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 9dd40336a..bb27633bb 100644
--- 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 ""