]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
source logging is now native in the interpreter
[helm.git] / helm / ocaml / mathql_interpreter / mQueryInterpreter.ml
index a5adbcd393ceaf14a0bb2be8460083bbc1873d49..d7ff053bd01061b8d16a21bc9dea72a8d5aef057 100644 (file)
@@ -233,6 +233,7 @@ 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 r = eval_query c x in