]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/topLevel/topLevel.ml
patches for the new interface of text_of_query/text_of result
[helm.git] / helm / gTopLevel / topLevel / topLevel.ml
index 338db29a7107a7ce8a15beb4be48ef2f843c682a..06ef93ab5f5571ec27a9455a2a7147c9773d7974 100644 (file)
@@ -16,7 +16,7 @@ let check_db () =
 
 let default_confirm q =
    let module Util = MQueryUtil in   
-   if ! show_queries then print_string (Util.text_of_query q ^ nl);
+   if ! show_queries then Util.text_of_query print_string q nl;
    let b = check_db () in
    if ! db_down then print_endline "db_down"; b 
 
@@ -79,7 +79,7 @@ let execute ich =
    Gen.set_confirm_query default_confirm;
    try 
       let q = Util.query_of_text (Lexing.from_channel ich) in
-      print_endline (Util.text_of_result (Gen.execute_query q) nl);
+      Util.text_of_result print_string (Gen.execute_query q) nl;
       flush stdout
    with Gen.Discard -> ()
 
@@ -88,7 +88,7 @@ let locate name =
    let module Gen = MQueryGenerator in
    Gen.set_confirm_query default_confirm;
    try 
-      print_endline (Util.text_of_result (Gen.locate name) nl);
+      Util.text_of_result print_string (Gen.locate name) nl;
       flush stdout
    with Gen.Discard -> ()
 
@@ -125,7 +125,7 @@ let mbackward n m l =
            let gen = List.nth info 1 in
            if Mqint.get_stat () then 
               print_string (num ^ " GEN = " ^ gen ^ ":" ^ string_of_float t1 ^ "s" ^ nl);
-           print_string (Util.text_of_result r nl);
+           Util.text_of_result print_string r nl;
             flush stdout
         with Gen.Discard -> ()
    in