]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/mQueryGenerator.ml
patches for the new interface of text_of_query/text_of result
[helm.git] / helm / gTopLevel / mQueryGenerator.ml
index 7e061eb0be302de929f024498d6d275f8edd13fb..ed52e55bda7e11825d8299628fcb2c6369d990c8 100644 (file)
@@ -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)