From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 26 Nov 2004 14:17:15 +0000 (+0000)
Subject: ported to Mysql
X-Git-Tag: PRE_UNIVERSES~10
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8eb9b5bc9507708e51c1d2d8616bb7b963aa6ff5;p=helm.git

ported to Mysql
---

diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml
index 0d959ac65..b19797df8 100644
--- 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 b6410fe3b..edfaa6927 100644
--- 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 c6b598151..7836fae47 100644
--- 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