mathql interpreter flags can be now red from helm registry

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

diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index a1ecd302f12525c8c96857d7dfdeb526d539a328..5e246c97c99d856d141cc08499b2358dea227615 100644 (file)
--- a/helm/gTopLevel/regtest.ml
+++ b/helm/gTopLevel/regtest.ml
@@ -154,9 +154,9 @@ let as_expected report_fname expected found = (* ignores "term" field *)
    end;
   outcome
 
-let test_this uri_pred raw_term =
+let test_this mqi_handle uri_pred raw_term =
   let empty_context = [] in
-  let (metasenv, cic_term) = BatchParser.parse ~uri_pred raw_term in
+  let (metasenv, cic_term) = BatchParser.parse mqi_handle ~uri_pred raw_term in
   let etype =
    try
     CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv empty_context cic_term)
@@ -202,7 +202,7 @@ let restore_environment filename =
   else
    CicEnvironment.empty ()
 
-let main generate dump fnames tryvars varsprefix =
+let main mqi_handle generate  dump fnames tryvars varsprefix =
  let uri_pred = BatchParser.uri_pred_of_conf tryvars varsprefix in
  if generate then
   begin
@@ -215,7 +215,7 @@ let main generate dump fnames tryvars varsprefix =
       print_endline (sprintf "Generating regtest %s -> %s\n ..."
         fname test_fname);
       let raw_term = (parse_regtest fname).term in
-      let result = test_this uri_pred raw_term in
+      let result = test_this mqi_handle uri_pred raw_term in
       print_test result test_fname ;
       if dump then dump_environment env_fname ;
     ) fnames
@@ -235,7 +235,7 @@ let main generate dump fnames tryvars varsprefix =
        let is_ok = 
         try
           let expected = parse_regtest test_fname in
-          let actual = test_this uri_pred expected.term in
+          let actual = test_this mqi_handle uri_pred expected.term in
           if dump then dump_environment env_fname ;
           if as_expected report_fname expected actual then
            (incr ok ; true)
@@ -265,6 +265,10 @@ let _ =
   (fun ?(append_NL = true) msg ->
     (if append_NL then prerr_endline else prerr_string)
       (HelmLogger.string_of_html_msg msg));
+ 
+ let mqi_debug_fun = ignore in
+ let mqi_handle = MQIConn.init mqi_debug_fun in
+ 
  let fnames = ref [] in
  let gen = ref false in
  let tryvars = ref false in
@@ -292,5 +296,5 @@ let _ =
   Arg.parse spec (fun filename -> fnames := filename::!fnames ) usage ;
   if !fnames = [] then
    Arg.usage spec (Sys.argv.(0) ^ ": missing argument test. You must provide at least one test file.\n" ^ usage) ;
-  main !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !varsprefix
-
+  main mqi_handle !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !varsprefix;
+  MQIConn.close mqi_handle