From 65828a2a9173bcdf3bf8f9100d0b9cd01109da94 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 13 Sep 2002 14:58:49 +0000 Subject: [PATCH] query generator timing feature improved --- helm/gTopLevel/mQueryGenerator.ml | 27 ++++++++++----------------- 1 file changed, 10 insertions(+), 17 deletions(-) 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 "" -- 2.39.2