- New interface for the MathQL interpreter (1.3 version)

[helm.git] / helm / gTopLevel / gTopLevel.ml

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 ()
 ;;