From d5edcb5c5314fe6cc79bdc5980aa561eaa8e600c Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 22 Oct 2004 12:54:46 +0000 Subject: [PATCH] - disambiguation now needs DBI handle - no longer build by default old cic_textual_parser --- helm/gTopLevel/disambiguatingParser.ml.in | 13 +++++++------ helm/gTopLevel/disambiguatingParser.mli | 2 +- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/helm/gTopLevel/disambiguatingParser.ml.in b/helm/gTopLevel/disambiguatingParser.ml.in index 6ba3b26ee..dfab60433 100644 --- a/helm/gTopLevel/disambiguatingParser.ml.in +++ b/helm/gTopLevel/disambiguatingParser.ml.in @@ -31,19 +31,19 @@ module AndreaAndZackDisambiguatingParser = module Make (C : DisambiguateTypes.Callbacks) = struct - let - disambiguate_term mqi_handle context metasenv term_as_string environment + let disambiguate_term ~(dbh:Dbi.connection) context metasenv term_as_string + aliases = - let module Disambiguate' = Disambiguate.Make (C) in + let module Disambiguate' = Disambiguate.Make (C) in let term = - CicTextualParser2.parse_term (Stream.of_string term_as_string) + CicTextualParser2.parse_term (Stream.of_string term_as_string) in - Disambiguate'.disambiguate_term - mqi_handle context metasenv term environment + Disambiguate'.disambiguate_term ~dbh context metasenv term ~aliases end end +(* module CSCTextualDisambiguatingParser = struct module EnvironmentP3 = OldDisambiguate.EnvironmentP3 @@ -97,6 +97,7 @@ module CSCTexDisambiguatingParser = context metasenv dom mk_metasenv_and_expr environment end end +*) @CHOSEN_TERM_PARSER@ diff --git a/helm/gTopLevel/disambiguatingParser.mli b/helm/gTopLevel/disambiguatingParser.mli index 620198a52..53b885088 100644 --- a/helm/gTopLevel/disambiguatingParser.mli +++ b/helm/gTopLevel/disambiguatingParser.mli @@ -36,7 +36,7 @@ module EnvironmentP3 : module Make (C : DisambiguateTypes.Callbacks) : sig val disambiguate_term : - MQIConn.handle -> + dbh:Dbi.connection -> Cic.context -> Cic.metasenv -> string -> -- 2.39.2