From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 22 Oct 2004 12:54:46 +0000 (+0000)
Subject: - disambiguation now needs DBI handle
X-Git-Tag: V_0_0_10~26
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d5edcb5c5314fe6cc79bdc5980aa561eaa8e600c;p=helm.git

- disambiguation now needs DBI handle
- no longer build by default old cic_textual_parser
---

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 ->