]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mquery_generator/mQueryGenerator.ml
MQueryInterpreter: interface updated
[helm.git] / helm / ocaml / mquery_generator / mQueryGenerator.ml
index ec9f98d1c3208aa0b9fd4882b4ae4caf6fe300f9..82363c987014f17d70f45dd83a0bfe4e92d0b080 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
-(*                                 30/04/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-module MQICallbacks =
-   struct
-      let log s = prerr_string s
-   end
-
-module MQI = MQueryInterpreter.Make(MQICallbacks)
+module MQI = MQueryInterpreter
 
 (* Query issuing functions **************************************************)
 
@@ -75,7 +60,7 @@ let set_confirm_query f =
 
 let get_query_info () = ! info
 
-let execute_query query =
+let execute_query handle query =
    let module Util = MQueryUtil in
    let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
    let perm = 64 * 6 + 8 * 6 + 4 in
@@ -98,7 +83,7 @@ let execute_query query =
       flush och 
    in
    let execute q =
-      let r = MQI.execute "" q in    
+      let r = MQI.execute handle q in    
       if ! log_file <> "" then log q r; 
       info := string_of_int ! query_num :: ! info;
       incr query_num;
@@ -108,14 +93,14 @@ let execute_query query =
                           
 (* Query building functions  ************************************************)   
 
-let locate s =
+let locate handle s =
    let module M = MathQL in
    let q =
     M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
    in
-    execute_query q
+    execute_query handle q
 
-let searchPattern must_use can_use =    
+let searchPattern handle must_use can_use =    
    let module M = MathQL in
    let in_path s = (s, []) in
    let assign v p = (in_path v, in_path p) in 
@@ -556,4 +541,4 @@ let searchPattern must_use can_use =
    (*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*)
 
 print_endline "### ";  MQueryUtil.text_of_query print_string (q_let_po opos 1) "\n"; flush stdout;
-   execute_query (q_let_po opos 1)
+   execute_query handle (q_let_po opos 1)