From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 22 Oct 2004 12:36:53 +0000 (+0000)
Subject: - no longer depends on MQueryMisc for term_of_uri
X-Git-Tag: V_0_0_10~35
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=095eaa933206f18b77cadd92260c6aea821d08cd;p=helm.git

- 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 02a51678b..f93043778 100644
--- 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 640549544..b7ef829a5 100644
--- 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 ->