From 8eb9b5bc9507708e51c1d2d8616bb7b963aa6ff5 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 26 Nov 2004 14:17:15 +0000 Subject: [PATCH] ported to Mysql --- helm/gTopLevel/batchParser.ml | 8 ++++---- helm/gTopLevel/batchParser.mli | 4 ++-- helm/gTopLevel/regtest.ml | 17 ++++++++++------- 3 files changed, 16 insertions(+), 13 deletions(-) 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 -- 2.39.2