batchParser and regtest patched to avoid a non encapsulated connection to the mathql...

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

diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml
index 61220eccef979b87372e520c2ef40ef62f0de4a4..1e301eaf945aa234146fef04e756105959f2525e 100644 (file)
--- a/helm/gTopLevel/batchParser.ml
+++ b/helm/gTopLevel/batchParser.ml
@@ -52,9 +52,9 @@ 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 mqi_handle = MQIConn.init mqi_flags mqi_debug_fun in
   uri_predicate := uri_pred;
   let empty_environment =
     DisambiguatingParser.EnvironmentP3.of_string
@@ -67,7 +67,7 @@ let parse ?(uri_pred = constants_only) =
       Disambiguate'.disambiguate_term
         mqi_handle empty_context empty_metasenv input empty_environment
     in
-    (metasenv, term)
+    MQIConn.close mqi_handle; (metasenv, term)
 
 let parse_pp ?uri_pred input = CicPp.ppterm (snd (parse ?uri_pred input))