mathql interpreter flags can be now red from helm registry

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

diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml
index 1e301eaf945aa234146fef04e756105959f2525e..7cbc31201ab39f1a3e98c3f27e27a7c3f74401a4 100644 (file)
--- a/helm/gTopLevel/batchParser.ml
+++ b/helm/gTopLevel/batchParser.ml
@@ -50,11 +50,7 @@ module DisambiguateCallbacks =
 
 module Disambiguate' = DisambiguatingParser.Make (DisambiguateCallbacks)
 
-let mqi_debug_fun = ignore
-let mqi_flags = []
-
-let parse ?(uri_pred = constants_only) =
-  let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun in
+let parse mqi_handle ?(uri_pred = constants_only) =
   uri_predicate := uri_pred;
   let empty_environment =
     DisambiguatingParser.EnvironmentP3.of_string
@@ -67,7 +63,8 @@ let parse ?(uri_pred = constants_only) =
       Disambiguate'.disambiguate_term
         mqi_handle empty_context empty_metasenv input empty_environment
     in
-    MQIConn.close mqi_handle; (metasenv, term)
+    (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))