From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 19 Feb 2004 15:49:01 +0000 (+0000)
Subject: source logging patched
X-Git-Tag: v0_0_4~130
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0aff38b3e5fefa68f5201e8852381e45882f55d2;p=helm.git

source logging patched
---

diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
index d7ff053bd..8a3a3b3cf 100644
--- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
+++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
@@ -233,9 +233,9 @@ let execute h x =
          try snd (List.assoc i c.avars) 
 	 with Not_found -> warn (M.AVar i); []
    in
-   let x = if C.set h C.Source then M.Log (false, true, x) else x 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
    let s = P.stop_time t in
    if C.set h C.Stat then