X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=4f6cab6afd292fc3d10752bbcc1d8a25f5b5a851;hb=09151f33b14507e4d20380f3100a6db5f49f3f46;hp=cfc11e921f79252b711180d13945a36e2ee46789;hpb=28f262128cd08dfaad435f73d3f4eee5976993d6;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index cfc11e921..4f6cab6af 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -37,16 +37,13 @@ open Printf;;
 
 (* DEBUGGING *)
 
-module MQICallbacks =
-   struct
-      let log s = prerr_string s
-   end
-
-module MQI = MQueryInterpreter.Make(MQICallbacks)
+module MQI = MQueryInterpreter
+module MQIC = MQIConn
 
 (* GLOBAL CONSTANTS *)
 
-let mqi_options = "" (* default MathQL interpreter options *)
+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";;
 
@@ -960,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,_ ->
@@ -1255,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:
@@ -1366,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:
@@ -1509,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 ->
@@ -1924,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 ->
@@ -1991,7 +1992,7 @@ let insertQuery () =
       None -> ()
     | Some q ->
        let results =
-        MQI.execute mqi_options (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
@@ -2139,6 +2140,7 @@ let searchPattern () =
       | Some metano ->
          let uris' =
            TacticChaser.searchPattern
+	    mqi_handle
             ~output_html:(output_html outputhtml) ~choose_must ()
             ~status:(proof, metano)
          in
@@ -2780,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 ->
@@ -2848,10 +2851,9 @@ let initialize_everything () =
 ;;
 
 let main () =
- if !usedb then ignore (MQI.init mqi_options) ;
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
- if !usedb then MQI.close mqi_options;
+ MQIC.close mqi_handle;
  Hbugs.quit ()
 ;;