MQueryInterpreter: interface updated

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

diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml
index afa47790ac3254173e4b2f708e8a2d570ba0d9f9..1e71be5b254b95738d00daf10000ddc8ae221525 100644 (file)
--- a/helm/gTopLevel/disambiguate.ml
+++ b/helm/gTopLevel/disambiguate.ml
@@ -77,8 +77,8 @@ type domain_and_interpretation =
 module Make(C:Callbacks) =
   struct
 
-   let locate_one_id id =
-    let result = MQueryGenerator.locate id in
+   let locate_one_id mqi_handle id =
+    let result = MQueryGenerator.locate mqi_handle id in
     let uris =
      List.map
       (function uri,_ ->
@@ -121,7 +121,7 @@ module Make(C:Callbacks) =
       Uris of CicTextualParser0.uri list
     | Symbols of (CicTextualParser0.interpretation -> Cic.term) list
 
-   let disambiguate_input context metasenv dom mk_metasenv_and_expr ~id_to_uris=
+   let disambiguate_input mqi_handle context metasenv dom mk_metasenv_and_expr ~id_to_uris=
     let known_ids,resolve_id = id_to_uris in
     let dom' =
      let rec filter =
@@ -136,7 +136,7 @@ module Make(C:Callbacks) =
      let list_of_uris =
       List.map
        (function
-           CicTextualParser0.Id id -> Uris (locate_one_id id)
+           CicTextualParser0.Id id -> Uris (locate_one_id mqi_handle id)
          | CicTextualParser0.Symbol (descr,choices) ->
             (* CSC: Implementare la funzione di filtraggio manuale *)
             (* CSC: corrispondente alla locate_one_id              *)