X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmquery_generator%2FmQueryGenerator.ml;h=378a8e264e5935716e07670a88a3eba082402abd;hb=fc3a73230e9c3a8359944ecbc5546f8f63acac25;hp=82363c987014f17d70f45dd83a0bfe4e92d0b080;hpb=ccff14650d0212aeadf0fcf6ef9ed2e792516686;p=helm.git

diff --git a/helm/ocaml/mquery_generator/mQueryGenerator.ml b/helm/ocaml/mquery_generator/mQueryGenerator.ml
index 82363c987..378a8e264 100644
--- a/helm/ocaml/mquery_generator/mQueryGenerator.ml
+++ b/helm/ocaml/mquery_generator/mQueryGenerator.ml
@@ -23,8 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-module MQI = MQueryInterpreter
-
 (* Query issuing functions **************************************************)
 
 type uri = string
@@ -40,68 +38,27 @@ type must_restrictions = (r_obj list * r_rel list * r_sort list)
 type only_restrictions =
  (r_obj list option * r_rel list option * r_sort list option)
 
-exception Discard  
-
-let nl = " <p>\n"
-
-let query_num = ref 1
-
-let log_file = ref ""
-
-let confirm_query = ref (fun _ -> true)
-
-let info = ref []
-
-let set_log_file f = 
-   log_file := f
+let builtin s = 
+   let ns = "h:" in
+   match s with
+      | "MH"   -> ns ^ "MainHypothesis"
+      | "IH"   -> ns ^ "InHypothesis"
+      | "MC"   -> ns ^ "MainConclusion"
+      | "IC"   -> ns ^ "InConclusion"
+      | "IB"   -> ns ^ "InBody"
+      | "SET"  -> ns ^ "Set"
+      | "PROP" -> ns ^ "Prop"
+      | "TYPE" -> ns ^ "Type"
+      | _      -> raise (Failure "MQueryGenerator.builtin")
 
-let set_confirm_query f =
-   confirm_query := f
-
-let get_query_info () = ! info
-
-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
-   let time () =
-      let lt = Unix.localtime (Unix.time ()) in
-      "NEW LOG: " ^
-      string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
-      string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
-      string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
-      string_of_int (lt.Unix.tm_hour) ^ ":" ^
-      string_of_int (lt.Unix.tm_min) ^ ":" ^
-      string_of_int (lt.Unix.tm_sec) 
-   in
-   let log q r = 
-      let och = open_out_gen mode perm ! log_file in
-      let out = output_string och in
-      if ! query_num = 1 then out (time () ^ nl);
-      out ("Query: " ^ string_of_int ! query_num ^ nl); Util.text_of_query out q nl; 
-      out ("Result:" ^ nl); Util.text_of_result out r nl; 
-      flush och 
-   in
-   let execute q =
-      let r = MQI.execute handle q in    
-      if ! log_file <> "" then log q r; 
-      info := string_of_int ! query_num :: ! info;
-      incr query_num;
-      r
-   in 
-   if ! confirm_query query then execute query else raise Discard
-                          
 (* Query building functions  ************************************************)   
 
-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 handle q
+module M = MathQL
+
+let locate s =
+   M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
 
-let searchPattern handle must_use can_use =    
-   let module M = MathQL in
+let searchPattern must_use can_use =    
    let in_path s = (s, []) in
    let assign v p = (in_path v, in_path p) in 
   
@@ -541,4 +498,4 @@ let searchPattern handle 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 handle (q_let_po opos 1)
+   (q_let_po opos 1)