From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 31 Oct 2002 14:24:15 +0000 (+0000)
Subject: MQueryGenerator ported to use fun "objectName"
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~4
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=36a85ffd9542d5a726d154cd8bf37d417da2cf88;p=helm.git

MQueryGenerator ported to use fun "objectName"
topLevel        typechecker output was removed
---

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 4deaf8c7a..9f52c2f20 100644
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -185,7 +185,7 @@ let execute_query query =
 
 let locate s =
    let module M = MathQL in
-   let q = M.Ref (M.Fun "reference" (M.Const [s])) in
+   let q = M.Ref (M.Fun "objectName" (M.Const [s])) in
    execute_query q
 
 let backward e c t level =
diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index d53ea70ea..6db896d9b 100644
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -196,7 +196,7 @@ let _ =
    CicCooking.init () ; 
    Logger.log_callback :=
       (Logger.log_to_html
-      ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
+      ~print_and_flush:(function s -> () (* print_string s ; flush stdout *) ));
    Mqint.set_stat false;
    Gen.set_log_file "MQGenLog.htm";
    set_dbms 1;