mathql query generator interface patched

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 9bd242eb8ad46ee3fa9e35934c28e089aaba663c..e3f49893171f5c9e1faaa01931ff9a76eef72a77 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -37,13 +37,15 @@ open Printf;;
 
 (* DEBUGGING *)
 
-let debug_print = 
-  let debug = true in
-  fun s -> prerr_endline (sprintf "DEBUG: %s" s)
-;;
+module MQI  = MQueryInterpreter
+module MQIC = MQIConn
+module MQG  = MQueryGenerator
 
 (* 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 +72,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;;
@@ -390,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
 =
@@ -963,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 ^
@@ -1258,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:
@@ -1369,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:
@@ -1512,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 ->
@@ -1520,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
@@ -1927,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 ->
@@ -1994,7 +1988,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 +2136,7 @@ let searchPattern () =
       | Some metano ->
          let uris' =
            TacticChaser.searchPattern
+           mqi_handle
             ~output_html:(output_html outputhtml) ~choose_must ()
             ~status:(proof, metano)
          in
@@ -2783,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 ->
@@ -2851,15 +2847,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 ()
 ;;