X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FmQueryGenerator.ml;h=ed52e55bda7e11825d8299628fcb2c6369d990c8;hb=a3ef256812f0397a871fe8e69c125dfd89e62dce;hp=7e061eb0be302de929f024498d6d275f8edd13fb;hpb=92515ddd2fc43f07f4dbb22c6bc98399ef1a2dd7;p=helm.git

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 7e061eb0b..ed52e55bd 100644
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -86,11 +86,10 @@ let execute_query query =
    in
    let log q r = 
       let och = open_out_gen mode perm ! log_file in
-      if ! query_num = 1 then output_string och (time () ^ nl);
-      let str =
-       "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^ 
-       "Result:" ^ nl ^ Util.text_of_result r nl in
-      output_string och str; 
+      let out = output_string och in
+      if ! query_num = 1 then out (time () ^ nl);
+      out ("Query: " ^ string_of_int ! query_num ^ nl); Util.text_of_query out q nl; 
+      out ("Result:" ^ nl); Util.text_of_result out r nl; 
       flush och 
    in
    let execute q =
@@ -551,5 +550,5 @@ let searchPattern must_use can_use =
    
    (*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*)
 
-print_endline ("### " ^ MQueryUtil.text_of_query (q_let_po opos 1)) ; flush stdout;
+print_endline "### ";  MQueryUtil.text_of_query print_string (q_let_po opos 1) "\n"; flush stdout;
    execute_query (q_let_po opos 1)