(* *)
(******************************************************************************)
-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 option
+type sort = string
-val close : unit -> unit (* CLOSE database function *)
+type r_obj = (uri * position * depth)
+type r_rel = (position * depth)
+type r_sort = (position * depth * sort)
-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 only_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 -> only_restrictions -> MathQL.result
+
+val get_query_info : unit -> string list