X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=f93043778bed0ce65060543805f2a54d78c0b499;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=93795f96ebb780eba031192d03ac15a16561a774;hpb=da49d2dca60a85abe54e0e549b290fa28a8127ba;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 93795f96e..f93043778 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -286,7 +286,7 @@ let interpretate ~context ~env ast =
   in
   match ast with
   | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
-  | term -> aux (-1, -1) context term
+  | term -> aux CicAst.dummy_floc context term
 
 let domain_of_term ~context ast =
     (* "aux" keeps domain in reverse order and doesn't care about duplicates.
@@ -400,8 +400,7 @@ let domain_of_term ~context ast =
   rev_uniq
     (match ast with
     | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
-    | term -> aux (-1, -1) context term)
-
+    | term -> aux CicAst.dummy_floc context term)
 
   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =
@@ -414,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
@@ -441,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 *)
@@ -472,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