X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FmQueryGenerator.mli;h=57137974f8ad0d7e12b88273ebcb956d4bd5fcbf;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=69cbfeba55e6f39496703fc96b84fd9697877adc;hpb=86ec68f575f6f781572d14d0aba9a98a860c94a6;p=helm.git

diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
index 69cbfeba5..57137974f 100644
--- a/helm/gTopLevel/mQueryGenerator.mli
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -33,17 +33,23 @@
 (*                                                                            *)
 (******************************************************************************)
 
-val levels    : Cic.metasenv -> Cic.context -> Cic.term -> string
-                                 (* level assignment testing function *)
+exception Discard  
 
-val call_back : (MathQL.mquery -> bool) -> unit
+type levels_spec = (string * bool * int) list
 
-val init      : unit -> unit     (* INIT database function *)
+val levels_of_term    : Cic.metasenv -> Cic.context -> Cic.term -> levels_spec
 
-val close     : unit -> unit     (* CLOSE database function *)
+val string_of_levels  : levels_spec -> string -> string
 
-val locate    : string -> MathQL.mqresult (* LOCATE query building function *)
-val locate_html : string -> string (* LOCATE query building function *)
+val set_log_file      : string -> unit
 
-val backward  : Cic.metasenv -> Cic.context -> Cic.term -> int -> string
-                                 (* BACKWARD query building function *)
+(* 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 backward          : Cic.metasenv -> Cic.context -> Cic.term -> int -> MathQL.result
+
+val get_query_info    : unit -> string list