- no longer depends on MQueryMisc for term_of_uri

- disambiguation now uses MetadataQuery instead of MathQL

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 02a51678b070429c89b9d6abbf4e15a7c3b4885f..f93043778bed0ce65060543805f2a54d78c0b499 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -413,15 +413,9 @@ let domain_diff dom1 dom2 =
 
 module Make (C: Callbacks) =
   struct
-    let choices_of_id mqi_handle id =
-     let query  =  MQueryGenerator.locate id in
-     let result = MQueryInterpreter.execute mqi_handle query in
-     let uris =
-      List.map
-       (function uri,_ ->
-         MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
-       ) result in
-      let uris' =
+    let choices_of_id dbh id =
+      let uris = MetadataQuery.locate ~dbh id in
+      let uris =
        match uris with
         | [] ->
            [UriManager.string_of_uri (C.input_or_locate_uri
@@ -440,13 +434,17 @@ module Make (C: Callbacks) =
           (uri,
            let term =
              try
-               HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri)
-             with _ -> assert false
+               CicUtil.term_of_uri uri
+             with exn ->
+               prerr_endline uri;
+               prerr_endline (Printexc.to_string exn);
+               assert false
             in
            fun _ _ _ -> term))
-        uris'
+        uris
 
-    let disambiguate_term mqi_handle context metasenv term ~aliases:current_env
+    let disambiguate_term ~(dbh:Dbi.connection) context metasenv term
+      ~aliases:current_env
     =
       debug_print "NEW DISAMBIGUATE INPUT";
       let disambiguate_context =  (* cic context -> disambiguate context *)
@@ -471,7 +469,7 @@ module Make (C: Callbacks) =
               (try
                 Hashtbl.find id_choices id
               with Not_found ->
-                let choices = choices_of_id mqi_handle id in
+                let choices = choices_of_id dbh id in
                 Hashtbl.add id_choices id choices;
                 choices)
           | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index 640549544c45c460c9724a7a72b0b13fabb5930b..b7ef829a519e1cfd4e08352cb5b197fc00d87ef8 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -32,7 +32,7 @@ exception NoWellTypedInterpretation
 module Make (C : Callbacks) :
   sig
     val disambiguate_term :
-      MQIConn.handle ->
+      dbh:Dbi.connection ->
       Cic.context ->
       Cic.metasenv ->
       CicAst.term ->