From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 5 Mar 2004 14:20:34 +0000 (+0000)
Subject: Debugging code removed.
X-Git-Tag: v0_0_4~44
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=45b8f3d3fcc007ffd2e7891b992444908aa1a2fd;p=helm.git

Debugging code removed.
Query logging is already implemented. It can be activated from the
.conf.xml file.
---

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 6a6ab9b27..e7d703663 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -404,13 +404,6 @@ module Make (C: Callbacks) =
        (function uri,_ ->
          MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
        ) result in
-      HelmLogger.log (`Msg (`T "Locate query:"));
-      MQueryUtil.text_of_query
-       (fun s -> HelmLogger.log ~append_NL:false (`Msg (`T s)))
-       "" query; 
-      HelmLogger.log (`Msg (`T "Result:"));
-      MQueryUtil.text_of_result
-        (fun s -> HelmLogger.log (`Msg (`T s))) "" result;
       let uris' =
        match uris with
         | [] ->