- New interface for the MathQL interpreter (1.3 version)

- Two toplevels committed in ocaml/mathql_test (new directory)

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 9bd242eb8ad46ee3fa9e35934c28e089aaba663c..cfc11e921f79252b711180d13945a36e2ee46789 100644 (file)
--- 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 d5917ee5027555efb5356fad89a90923a2ba9cda..4775ab302436ca330d1e13a6f6a7582420cc7bb4 100644 (file)
--- 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 ed52e55bda7e11825d8299628fcb2c6369d990c8..ec9f98d1c3208aa0b9fd4882b4ae4caf6fe300f9 100644 (file)
--- 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 35270fd62c8ee31d46ca2469a819b94e57ebfeb8..5e742b243a6b9d04c0b1f6b96a5c89d92e49dda4 100644 (file)
--- 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