From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Jun 2003 17:54:03 +0000 (+0000)
Subject: * mquery_interpreter logging and debugging activated
X-Git-Tag: V7_3_new_exportation_merged~10
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=4fa5b9f1173f4d45c0f01d573392c9adcb4269eb

* mquery_interpreter logging and debugging activated
* bug fixed: the universe of the complete search pattern must exclude
  the InBody occurrences
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e3f498931..83947a24a 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -43,7 +43,10 @@ module MQG  = MQueryGenerator
 
 (* GLOBAL CONSTANTS *)
 
+let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
+(*
 let mqi_flags = [] (* default MathQL interpreter options *)
+*)
 let mqi_handle = MQIC.init mqi_flags prerr_string
 
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
@@ -1920,7 +1923,16 @@ let completeSearchPattern () =
    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
    let must = MQueryLevels2.get_constraints expr in
    let must',only = refine_constraints must in
-   let query = MQG.query_of_constraints None must' only in
+   let query =
+    MQG.query_of_constraints
+     (Some
+       ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
+        "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis" ;
+        "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" ;
+        "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis"
+       ])
+     must' only
+   in
    let results = MQI.execute mqi_handle query in 
     show_query_results results
   with