...

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

diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml
index bd7165becc4e7982a6b86ae78ac69d16e006b8ad..7cbc31201ab39f1a3e98c3f27e27a7c3f74401a4 100644 (file)
--- a/helm/gTopLevel/batchParser.ml
+++ b/helm/gTopLevel/batchParser.ml
@@ -40,11 +40,6 @@ let uri_pred_of_conf tryvars varsprefix =
 
 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
@@ -55,11 +50,7 @@ module DisambiguateCallbacks =
 
 module Disambiguate' = DisambiguatingParser.Make (DisambiguateCallbacks)
 
-let mqi_debug_fun = ignore
-let mqi_flags = []
-let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun
-
-let parse ?(uri_pred = constants_only) =
+let parse mqi_handle ?(uri_pred = constants_only) =
   uri_predicate := uri_pred;
   let empty_environment =
     DisambiguatingParser.EnvironmentP3.of_string
@@ -74,5 +65,6 @@ let parse ?(uri_pred = constants_only) =
     in
     (metasenv, term)
 
-let parse_pp ?uri_pred input = CicPp.ppterm (snd (parse ?uri_pred input))
+let parse_pp mqi_handle ?uri_pred input = 
+   CicPp.ppterm (snd (parse mqi_handle ?uri_pred input))