Added () to MQInit.init.

[helm.git] / helm / gTopLevel / testlibrary.ml

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index 7f23b2f12e165893e5a33289c66aa4bbbeddd055..a60aada5d3380d26222767970cc78c1efe3d6ac5 100644 (file)
--- a/helm/gTopLevel/testlibrary.ml
+++ b/helm/gTopLevel/testlibrary.ml
@@ -3,7 +3,7 @@ open Printf
 
 let mqi_debug_fun = ignore
 let mqi_flags = []
-let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun
+let mqi_handle = MQIConn.init ~flags:mqi_flags ~log:mqi_debug_fun ()
 
 let verbose = false
 
@@ -15,17 +15,12 @@ let uri_predicate = ref BatchParser.constants_only
 
 module DisambiguateCallbacks =
  struct
-  let output_html ?(append_NL = true) msg =
-    if verbose then
-      (if append_NL then print_string else print_endline)
-        (Ui_logger.string_of_html_msg msg)
-
   let interactive_user_uri_choice
    ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices =
      List.filter !uri_predicate choices
 
   let interactive_interpretation_choice _ = raise Multiple_interpretations
-  let input_or_locate_uri ~title = fail "Unknown identifier"
+  let input_or_locate_uri ~title = fail ("Unknown identifier: " ^ title)
  end
 
 module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
@@ -43,9 +38,12 @@ let test_uri uri =
     let (ast, _) =
       Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
     in
-    debug_print ("ast: " ^ CicAstPp.pp_term ast);
+    let new_pp = BoxPp.pp_term ast in
+    debug_print ("ast:\n" ^ new_pp);
+    let new_ast = CicTextualParser2.parse_term (Stream.of_string new_pp) in
+    debug_print ("new_ast:\n" ^ CicAstPp.pp_term ast);
     let (_, _, term) =
-      Disambiguate'.disambiguate_term mqi_handle [] [] ast
+      Disambiguate'.disambiguate_term mqi_handle [] [] new_ast
         DisambiguateTypes.Environment.empty
     in
     debug_print ("term: " ^ CicPp.ppterm term)
@@ -132,6 +130,11 @@ let do_file status fname =
       fname (Printexc.to_string exn)
 
 let _ =
+  Helm_registry.load_from "triciclo.conf.xml";
+  HelmLogger.register_log_callback
+   (fun ?(append_NL = true) msg ->
+     (if append_NL then prerr_endline else prerr_string)
+       (HelmLogger.string_of_html_msg msg));
   let names = ref [] in
   let tryvars = ref false in
   let varsprefix = ref "" in