]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mquery_generator/mQueryGenerator.mli
MathQL query generator: new interface
[helm.git] / helm / ocaml / mquery_generator / mQueryGenerator.mli
index 37a98adec20a68be77f5f98e400fc23e01cac12a..e1ad25caf5f6b871df237ea8b686a0fa57f1a22d 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
-(*                                 30/04/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-exception Discard  
-
 type uri = string
 type position = string
 type depth = int option
@@ -48,17 +36,8 @@ 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)
 
+val locate        : string -> MathQL.query
 
+val searchPattern : must_restrictions -> only_restrictions -> MathQL.query
 
-val set_log_file      : string -> unit
-
-(* the callback function must return false iff the query must be skipped *)
-val set_confirm_query : (MathQL.query -> bool) -> unit
-
-val execute_query     : MQIConn.handle -> MathQL.query -> MathQL.result
-
-val locate            : MQIConn.handle -> string -> MathQL.result
-
-val searchPattern     : MQIConn.handle -> must_restrictions -> only_restrictions -> MathQL.result
-
-val get_query_info    : unit -> string list
+val builtin       : MathQL.vvar -> string