X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=cfc11e921f79252b711180d13945a36e2ee46789;hb=a69b6f01bfeda05c431325a5defb5c5592427791;hp=9bd242eb8ad46ee3fa9e35934c28e089aaba663c;hpb=718bc0ea70defa418c23850dbb8f2850b0c3a542;p=helm.git

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