ported to Mysql

diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml
index 0d959ac6540861dbd31bdb9843079ca89a56673f..b19797df8bd3a3341e708533052dd9cf88db5101 100644 (file)
--- a/helm/gTopLevel/batchParser.ml
+++ b/helm/gTopLevel/batchParser.ml
@@ -71,7 +71,7 @@ module DisambiguateCallbacks =
 
 module Disambiguate' = DisambiguatingParser.Make (DisambiguateCallbacks)
 
-let parse mqi_handle ?(uri_pred = constants_only ~prefix:"") =
+let parse dbd ?(uri_pred = constants_only ~prefix:"") =
   uri_predicate := uri_pred;
   let empty_environment =
     DisambiguatingParser.EnvironmentP3.of_string
@@ -81,9 +81,9 @@ let parse mqi_handle ?(uri_pred = constants_only ~prefix:"") =
   let empty_metasenv = [] in
   fun input ->
    (Disambiguate'.disambiguate_term
-     mqi_handle empty_context empty_metasenv input empty_environment)
+     dbd empty_context empty_metasenv input empty_environment)
 
-let parse_pp mqi_handle ?uri_pred input = 
+let parse_pp dbd ?uri_pred input = 
  List.map (fun (_,_,t) -> CicPp.ppterm t)
-  (parse mqi_handle ?uri_pred input)
+  (parse dbd ?uri_pred input)
 

diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli
index b6410fe3bc1af096d6e6b8ae4c1c9847c9e9a989..edfaa69272d3b032fa1da3604e86db93fde7a7bf 100644 (file)
--- a/helm/gTopLevel/batchParser.mli
+++ b/helm/gTopLevel/batchParser.mli
@@ -39,11 +39,11 @@ val uri_pred_of_conf:
    * uri_pred is the predicate used to select which uris are tried. Per default
    * only constant URIs are accepted *)
 val parse:
- MQIConn.handle -> ?uri_pred:(string -> bool) -> string ->
+ Mysql.dbd -> ?uri_pred:(string -> bool) -> string ->
   (DisambiguatingParser.EnvironmentP3.t * Cic.metasenv * Cic.term) list
 
   (** as above, but instead of returning the parsed cic term, pretty prints it
    * (ignoring returned metasenv)
    *)
-val parse_pp: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> string list
+val parse_pp: Mysql.dbd -> ?uri_pred:(string -> bool) -> string -> string list
 

diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index c6b598151b2127babf3df6f449274fe41c857caa..7836fae472848fa423dd923e2437f7ab8f96aac6 100644 (file)
--- a/helm/gTopLevel/regtest.ml
+++ b/helm/gTopLevel/regtest.ml
@@ -338,11 +338,14 @@ 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 s =
-  HelmLogger.log ~append_NL:true (`Msg (`T s)) in
- let mqi_handle = MQIConn.init ~log:mqi_debug_fun () in
- 
+ Helm_registry.load_from "gTopLevel.conf.xml";
+ let dbd =
+  Mysql.quick_connect
+    ~host:(Helm_registry.get "db.host")
+    ~user:(Helm_registry.get "db.user")
+    ~database:(Helm_registry.get "db.database")
+    ()
+ in
  let fnames = ref [] in
  let gen = ref false in
  let tryvars = ref false in
@@ -376,5 +379,5 @@ let _ =
   if !fnames = [] then
    Arg.usage spec (Sys.argv.(0) ^ ": missing argument test. You must provide at least one test file.\n" ^ usage) ;
   if !varsprefix = "###" then varsprefix := !prefix ;
-  main mqi_handle !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !prefix !varsprefix;
-  MQIConn.close mqi_handle
+  main dbd !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !prefix !varsprefix;
+  Mysql.disconnect dbd