]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/testlibrary.ml
new getter, logger, and the hell
[helm.git] / helm / gTopLevel / testlibrary.ml
index 7f23b2f12e165893e5a33289c66aa4bbbeddd055..5abdec6e183935b77ca6a9925f8ec2de97ec3f0c 100644 (file)
@@ -15,11 +15,6 @@ 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
@@ -132,6 +127,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