X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2FmQueryInterpreter.ml;h=9280a2c2acdaa86c0aaf37eb00e563c74c301815;hb=951069678fea0d6dcdde984320ec5057ddc57c3c;hp=a5adbcd393ceaf14a0bb2be8460083bbc1873d49;hpb=6e2770c280aa9e74604e25324afb680b18d01964;p=helm.git diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml index a5adbcd39..9280a2c2a 100644 --- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml +++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + (* contexts *****************************************************************) type svar_context = (MathQL.svar * MathQL.resource_set) list @@ -133,7 +135,7 @@ let execute h x = let t = P.start_time () in P.text_of_query (C.log h) "\n" x; let s = P.stop_time t in - if C.set h C.Stat then + if C.set h C.Times then C.log h (Printf.sprintf "Log source: %s\n" s); eval_query c x end else begin @@ -141,7 +143,7 @@ let execute h x = let t = P.start_time () in P.text_of_result (C.log h) "\n" s; let r = P.stop_time t in - if C.set h C.Stat then + if C.set h C.Times then C.log h (Printf.sprintf "Log: %s\n" r); s end @@ -196,7 +198,7 @@ let execute h x = let t = P.start_time () in let r = MQIProperty.exec h q1 subj cons_true cons_false exp in let s = P.stop_time t in - if C.set h C.Stat then + if C.set h C.Times then C.log h (Printf.sprintf "Property: %s,%i\n" s (List.length r)); r | M.StatQuery x -> @@ -234,10 +236,12 @@ let execute h x = with Not_found -> warn (M.AVar i); [] in let c = {svars = []; avars = []; groups = []; vvars = []} in - let t = P.start_time () in + let t = P.start_time () in + if C.set h C.Source then P.text_of_query (C.log h) "\n" x; let r = eval_query c x in + if C.set h C.Result then P.text_of_result (C.log h) "\n" r; let s = P.stop_time t in - if C.set h C.Stat then + if C.set h C.Times then C.log h (Printf.sprintf "MQIExecute: %s,%s\n" s (C.string_of_flags (C.flags h))); r