From 095eaa933206f18b77cadd92260c6aea821d08cd Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 22 Oct 2004 12:36:53 +0000 Subject: [PATCH] - no longer depends on MQueryMisc for term_of_uri - disambiguation now uses MetadataQuery instead of MathQL --- helm/ocaml/cic_disambiguation/disambiguate.ml | 26 +++++++++---------- .../ocaml/cic_disambiguation/disambiguate.mli | 2 +- 2 files changed, 13 insertions(+), 15 deletions(-) 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 -> -- 2.39.2