X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql_test%2Fmqgtop.ml;h=bb776474761377a2fca8451524889a9e09b4398f;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=aba3bb3d4e85846ec70f31f2ca1725713cb48627;hpb=506b4b7597021c98e34fb65cf9d0bb7879f06e92;p=helm.git

diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml
index aba3bb3d4..bb7764747 100644
--- a/helm/mathql_test/mqgtop.ml
+++ b/helm/mathql_test/mqgtop.ml
@@ -52,8 +52,8 @@ module C1 = CGMatchConclusion
 module GU = MQGUtil
 
 let get_handle () = 
-   C.init (C.flags_of_string ! int_options)
-          (fun s -> print_string s; flush stdout) 
+   C.init ~flags:(C.flags_of_string ! int_options)
+          ~log:(fun s -> print_string s; flush stdout) () 
              
 let issue handle q =
    let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
@@ -73,14 +73,14 @@ let issue handle q =
       let out = output_string och in 
       if ! query_num = 1 then out (time () ^ nl);
       out ("Query: " ^ string_of_int ! query_num ^ nl);
-      U.text_of_query out q nl;
+      U.text_of_query out nl q;
       out ("Result: " ^ nl);
-      U.text_of_result out r nl;
+      U.text_of_result out nl r;
       close_out och
    in
-   if ! show_queries then U.text_of_query (output_string stdout) q nl;
+   if ! show_queries then U.text_of_query (output_string stdout) nl q;
    let r = I.execute handle q in    
-   U.text_of_result (output_string stdout) r nl;
+   U.text_of_result (output_string stdout) nl r;
    if ! log_file <> "" then log q r; 
    incr query_num;
    flush stdout
@@ -232,7 +232,7 @@ let mbackward n m l =
 
 let inductive l = 
    let queries = ref [] in
-   let univ = Some C3.universe in 
+   let univ = None in 
    let handle = get_handle () in
    let rec aux = function
       | []           -> ()
@@ -324,10 +324,13 @@ let rec parse = function
    | _ :: rem -> parse rem
 
 let _ =
+   Helm_registry.load_from "/home/fguidi/miohelm/gTopLevel.conf.xml";
    let t = U.start_time () in
-   Logger.log_callback :=
-      (Logger.log_to_html 
+(*
+   CicLogger.log_callback :=
+      (CicLogger.log_to_html 
        ~print_and_flush:(fun s -> print_string s; flush stdout)) ; 
+*)
    parse (List.tl (Array.to_list Sys.argv)); 
    prerr_endline ("mqgtop: done in " ^ (U.stop_time t));
    exit 0