From a69b6f01bfeda05c431325a5defb5c5592427791 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 23 Apr 2003 11:05:32 +0000 Subject: [PATCH] - New interface for the MathQL interpreter (1.3 version) - Two toplevels committed in ocaml/mathql_test (new directory) --- helm/gTopLevel/gTopLevel.ml | 30 +++++++------------ helm/ocaml/Makefile.in | 2 +- .../ocaml/mquery_generator/mQueryGenerator.ml | 9 ++++-- helm/searchEngine/searchEngine.ml | 21 ++++++------- 4 files changed, 30 insertions(+), 32 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 9bd242eb8..cfc11e921 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -37,13 +37,17 @@ open Printf;; (* DEBUGGING *) -let debug_print = - let debug = true in - fun s -> prerr_endline (sprintf "DEBUG: %s" s) -;; +module MQICallbacks = + struct + let log s = prerr_string s + end + +module MQI = MQueryInterpreter.Make(MQICallbacks) (* GLOBAL CONSTANTS *) +let mqi_options = "" (* default MathQL interpreter options *) + let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; let htmlheader = @@ -70,13 +74,6 @@ let prooffiletype = Not_found -> "/public/currentprooftype" ;; -let postgresqlconnectionstring = - try - Sys.getenv "POSTGRESQL_CONNECTION_STRING" - with - Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" -;; - (* GLOBAL REFERENCES (USED BY CALLBACKS) *) let htmlheader_and_content = ref htmlheader;; @@ -1994,7 +1991,7 @@ let insertQuery () = None -> () | Some q -> let results = - Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q)) + MQI.execute mqi_options (MQueryUtil.query_of_text (Lexing.from_string q)) in show_query_results results with @@ -2851,15 +2848,10 @@ let initialize_everything () = ;; let main () = - if !usedb then - begin - Mqint.set_database Mqint.postgres_db ; - Mqint.init postgresqlconnectionstring ; - end ; + if !usedb then ignore (MQI.init mqi_options) ; ignore (GtkMain.Main.init ()) ; initialize_everything () ; - if !usedb then Mqint.close (); - prerr_endline "FOO"; + if !usedb then MQI.close mqi_options; Hbugs.quit () ;; diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index d5917ee50..4775ab302 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -2,7 +2,7 @@ MODULES = xml urimanager getter pxp cic cic_annotations cic_annotations_cache \ cic_cache cic_proof_checking cic_textual_parser \ tex_cic_textual_parser cic_unification mathql mathql_interpreter \ - mquery_generator tactics + mquery_generator mathql_test tactics OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ OCAMLFIND_META_DIR = @OCAMLFIND_META_DIR@ diff --git a/helm/ocaml/mquery_generator/mQueryGenerator.ml b/helm/ocaml/mquery_generator/mQueryGenerator.ml index ed52e55bd..ec9f98d1c 100644 --- a/helm/ocaml/mquery_generator/mQueryGenerator.ml +++ b/helm/ocaml/mquery_generator/mQueryGenerator.ml @@ -33,9 +33,14 @@ (* *) (******************************************************************************) -(* Query issuing functions **************************************************) +module MQICallbacks = + struct + let log s = prerr_string s + end +module MQI = MQueryInterpreter.Make(MQICallbacks) +(* Query issuing functions **************************************************) type uri = string type position = string @@ -93,7 +98,7 @@ let execute_query query = flush och in let execute q = - let r = Mqint.execute q in + let r = MQI.execute "" q in if ! log_file <> "" then log q r; info := string_of_int ! query_num :: ! info; incr query_num; diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 35270fd62..5e742b243 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -33,14 +33,16 @@ Http_common.debug := true;; (** accepted HTTP servers for ask_uwobo method forwarding *) let valid_servers = [ "mowgli.cs.unibo.it:58080" ; "mowgli.cs.unibo.it" ; "localhost:58080" ] ;; -open Printf;; +module MQICallbacks = + struct + let log s = debug_print s + end -let postgresConnectionString = - try - Sys.getenv "POSTGRESQL_CONNECTION_STRING" - with - Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" -;; +module MQI = MQueryInterpreter.Make(MQICallbacks) + +let mqi_options = "" (* default MathQL interpreter options *) + +open Printf;; let daemon_name = "Search Engine";; let default_port = 58085;; @@ -182,7 +184,7 @@ let callback (req: Http_types.request) outchan = try debug_print (sprintf "Received request: %s" req#path); if req#path <> "/getpage" then - Mqint.init postgresConnectionString; + ignore (MQI.init mqi_options); (match req#path with | "/execute" -> let query_string = req#param "query" in @@ -440,7 +442,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; | invalid_request -> Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan); if req#path <> "/getpage" then - Mqint.close (); + MQI.close mqi_options; debug_print (sprintf "%s done!" req#path) with | Chat_unfinished -> prerr_endline "Chat unfinished, Try again!" @@ -456,7 +458,6 @@ printf "Current directory is %s\n" (Sys.getcwd ()); printf "HTML directory is %s\n" pages_dir; flush stdout; Unix.putenv "http_proxy" ""; -Mqint.set_database Mqint.postgres_db; Http_daemon.start' ~port callback; printf "%s is terminating, bye!\n" daemon_name -- 2.39.2