*** empty log message ***

[helm.git] / helm / gTopLevel / mQueryGenerator.mli

diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
index 0282c3c8dacf71dac985810d17d4d5eb29145dd9..e6b98c2eaa77ffb1cbcb697adc30f867f9f84dcc 100644 (file)
--- a/helm/gTopLevel/mQueryGenerator.mli
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -33,15 +33,36 @@
 (*                                                                            *)
 (******************************************************************************)
 
-val levels  : Cic.metasenv -> Cic.context -> Cic.term -> int -> string
-                                 (* level assignment testing function *)
+exception Discard  
 
-val init      : unit -> unit     (* INIT database function *)
+type uri = string
+type position = string
+type depth = int
+type sort = string 
 
-val close     : unit -> unit     (* CLOSE database function *)
+type r_obj = (uri * position * depth option) 
+type r_rel = (position * depth)
+type r_sort = (position * depth * sort) 
+(*
+type r_obj = (string * string * int option) 
+type r_rel = (string * int) 
+type r_sort = (string * int * string) 
+*)
 
-val locate    : string -> MathQL.mqresult (* LOCATE query building function *)
-val locate_html : string -> string (* LOCATE query building function *)
+type must_restrictions = (r_obj list * r_rel list * r_sort list)
+type can_restrictions = (r_obj list option * r_rel list option * r_sort list option)
 
-val backward  : Cic.metasenv -> Cic.context -> Cic.term -> int -> string
-                                 (* BACKWARD query building function *)
+
+
+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     : MathQL.query -> MathQL.result
+
+val locate            : string -> MathQL.result
+
+val searchPattern     : must_restrictions -> can_restrictions -> MathQL.result
+
+val get_query_info    : unit -> string list