mathql query generator interface patched

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index cfc11e921f79252b711180d13945a36e2ee46789..e3f49893171f5c9e1faaa01931ff9a76eef72a77 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -37,16 +37,14 @@ open Printf;;
 
 (* DEBUGGING *)
 
-module MQICallbacks =
-   struct
-      let log s = prerr_string s
-   end
-
-module MQI = MQueryInterpreter.Make(MQICallbacks)
+module MQI  = MQueryInterpreter
+module MQIC = MQIConn
+module MQG  = MQueryGenerator
 
 (* 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";;
 
@@ -387,19 +385,6 @@ let interactive_interpretation_choice interpretations =
 
 (* MISC FUNCTIONS *)
 
-(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
-(* FG : THIS FUNCTION IS BECOMING A REAL NONSENSE                   *)
-let get_last_query = 
- let query = ref "" in
-  let out s = query := ! query ^ s in
-  MQueryGenerator.set_confirm_query
-   (function q -> 
-    query := ""; MQueryUtil.text_of_query out q ""; true);
-  function result ->
-   out (!query ^ " <h1>Result:</h1> "); MQueryUtil.text_of_result out result "<br>";
-   !query
-;;
-
 let
  save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
 =
@@ -960,16 +945,18 @@ 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 out = output_html outputhtml in
+ let query = MQG.locate id in
+ let result = MQI.execute mqi_handle query in
  let uris =
   List.map
    (function uri,_ ->
      MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
    result in
- let html =
-  (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
- in
-  output_html outputhtml html ;
+  out "<h1>Locate Query: </h1><pre>";
+  MQueryUtil.text_of_query out query ""; 
+  out "<h1>Result:</h1>";
+  MQueryUtil.text_of_result out result "<br>";
   user_uri_choice ~title:"Ambiguous input."
    ~msg:
      ("Ambiguous input \"" ^ id ^
@@ -1255,6 +1242,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 +1354,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 +1498,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 ->
@@ -1517,7 +1508,12 @@ let new_proof () =
       okb#misc#set_sensitive (b && uri_entry#text <> ""))
  in
  let _ =
+let xxx = inputt#get_as_string in
+prerr_endline ("######################## " ^ xxx) ;
+  newinputt#set_term xxx ;
+(*
   newinputt#set_term inputt#get_as_string ;
+*)
   inputt#reset in
  let _ =
   uri_entry#connect#changed
@@ -1924,7 +1920,8 @@ 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 query = MQG.query_of_constraints None must' only in
+   let results = MQI.execute mqi_handle query in 
     show_query_results results
   with
    e ->
@@ -1991,7 +1988,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 +2136,7 @@ let searchPattern () =
       | Some metano ->
          let uris' =
            TacticChaser.searchPattern
+           mqi_handle
             ~output_html:(output_html outputhtml) ~choose_must ()
             ~status:(proof, metano)
          in
@@ -2780,6 +2778,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 +2847,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 ()
 ;;