MQueryInterpreter: interface updated

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 9bd242eb8ad46ee3fa9e35934c28e089aaba663c..4f6cab6afd292fc3d10752bbcc1d8a25f5b5a851 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -37,13 +37,14 @@ open Printf;;
 
 (* DEBUGGING *)
 
-let debug_print = 
-  let debug = true in
-  fun s -> prerr_endline (sprintf "DEBUG: %s" s)
-;;
+module MQI = MQueryInterpreter
+module MQIC = MQIConn
 
 (* GLOBAL CONSTANTS *)
 
+let mqi_flags = [] (* default MathQL interpreter options *)
+let mqi_handle = MQIC.init mqi_flags prerr_string
+
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
 
 let htmlheader =
@@ -70,13 +71,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;;
@@ -963,7 +957,7 @@ let user_uri_choice ~title ~msg uris =
 
 let locate_callback id =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let result = MQueryGenerator.locate id in
+ let result = MQueryGenerator.locate mqi_handle id in
  let uris =
   List.map
    (function uri,_ ->
@@ -1258,6 +1252,7 @@ let new_inductive () =
         ~packing:(vbox#pack ~expand:true ~padding:0) () in
       let newinputt =
        TexTermEditor'.term_editor
+        mqi_handle
         ~width:400 ~height:20 ~packing:scrolled_window#add 
         ~share_id_to_uris_with:inputt ()
         ~isnotempty_callback:
@@ -1369,6 +1364,7 @@ let new_inductive () =
         ~packing:(vbox#pack ~expand:true ~padding:0) () in
       let newinputt =
        TexTermEditor'.term_editor
+        mqi_handle
         ~width:400 ~height:20 ~packing:scrolled_window#add
         ~share_id_to_uris_with:inputt ()
         ~isnotempty_callback:
@@ -1512,7 +1508,9 @@ let new_proof () =
    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
  (* moved here to have visibility of the ok button *)
  let newinputt =
-  TexTermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
+  TexTermEditor'.term_editor
+   mqi_handle
+   ~width:400 ~height:100 ~packing:scrolled_window#add
    ~share_id_to_uris_with:inputt ()
    ~isnotempty_callback:
     (function b ->
@@ -1927,7 +1925,7 @@ let completeSearchPattern () =
    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
    let must = MQueryLevels2.get_constraints expr in
    let must',only = refine_constraints must in
-   let results = MQueryGenerator.searchPattern must' only in 
+   let results = MQueryGenerator.searchPattern mqi_handle must' only in 
     show_query_results results
   with
    e ->
@@ -1994,7 +1992,7 @@ let insertQuery () =
       None -> ()
     | Some q ->
        let results =
-        Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q))
+        MQI.execute mqi_handle (MQueryUtil.query_of_text (Lexing.from_string q))
        in
         show_query_results results
   with
@@ -2142,6 +2140,7 @@ let searchPattern () =
       | Some metano ->
          let uris' =
            TacticChaser.searchPattern
+           mqi_handle
             ~output_html:(output_html outputhtml) ~choose_must ()
             ~status:(proof, metano)
          in
@@ -2783,6 +2782,7 @@ class rendering_window output (notebook : notebook) =
    ~packing:frame#add () in
  let inputt =
   TexTermEditor'.term_editor
+   mqi_handle
    ~width:400 ~height:100 ~packing:scrolled_window1#add ()
    ~isnotempty_callback:
     (function b ->
@@ -2851,15 +2851,9 @@ let initialize_everything () =
 ;;
 
 let main () =
- if !usedb then
-  begin
-   Mqint.set_database Mqint.postgres_db ;
-   Mqint.init postgresqlconnectionstring ;
-  end ;
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
- if !usedb then Mqint.close ();
- prerr_endline "FOO";
+ MQIC.close mqi_handle;
  Hbugs.quit ()
 ;;