MQueryInterpreter: interface updated

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

diff --git a/helm/gTopLevel/disambiguate.mli b/helm/gTopLevel/disambiguate.mli
index 63206cb154e31b3d272797366cedf68b89408d9f..9fdfb8993dae6cdf8eaf7c57a97414d96259955b 100644 (file)
--- a/helm/gTopLevel/disambiguate.mli
+++ b/helm/gTopLevel/disambiguate.mli
@@ -33,18 +33,17 @@
 (*                                                                            *)
 (******************************************************************************)
 
-(** Functions that should be moved in another module **)
-exception IllFormedUri of string
-val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string
-val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri
-
-val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string
-
 (** This module provides a functor to disambiguate the input **)
 (** given a set of user-interface call-backs                 **)
 
 module type Callbacks =
   sig
+    (* The following two functions are used to save/restore the metasenv *)
+    (* before/after the parsing.                                         *)
+    (*CSC: This should be made functional sooner or later! *)
+    val get_metasenv : unit -> Cic.metasenv
+    val set_metasenv : Cic.metasenv -> unit
+
     val output_html : string -> unit
     val interactive_user_uri_choice :
       selection_mode:[`SINGLE | `EXTENDED] ->
@@ -57,18 +56,18 @@ module type Callbacks =
   end
 
 type domain_and_interpretation =
- string list * (string -> CicTextualParser0.uri option)
+ CicTextualParser0.interpretation_domain_item list *
+  CicTextualParser0.interpretation
 
-module Make :
-  functor (C : Callbacks) ->
+module Make (C : Callbacks) :
     sig
       exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
       val disambiguate_input :
+        MQIConn.handle -> 
         Cic.context ->
         Cic.metasenv ->
-        string list ->
-        ((string -> CicTextualParser0.interp_codomain option) ->
-         Cic.metasenv * Cic.term) ->
+        CicTextualParser0.interpretation_domain_item list ->
+        (CicTextualParser0.interpretation -> Cic.metasenv * Cic.term) ->
         id_to_uris:domain_and_interpretation ->
         domain_and_interpretation * Cic.metasenv * Cic.term
     end