From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 20 May 2002 10:48:31 +0000 (+0000)
Subject: mquery.ml now really call the execution of the query.
X-Git-Tag: V_0_3_0_debian_8~97
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=4afb38bb0927c06ab4e64656f31cfc0fcb089b1e

mquery.ml now really call the execution of the query.
Locate and backward now really work!!!
---

diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend
index e2b5d7730..63ec81c6c 100644
--- a/helm/gTopLevel/.depend
+++ b/helm/gTopLevel/.depend
@@ -4,8 +4,8 @@ logicalOperations.cmo: proofEngine.cmo
 logicalOperations.cmx: proofEngine.cmx 
 sequentPp.cmo: cic2Xml.cmo cic2acic.cmo proofEngine.cmo 
 sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx 
-mquery.cmo: mathql.cmo mquery.cmi 
-mquery.cmx: mathql.cmx mquery.cmi 
+mquery.cmo: mquery.cmi 
+mquery.cmx: mquery.cmi 
 gTopLevel.cmo: cic2Xml.cmo cic2acic.cmo logicalOperations.cmo mquery.cmi \
     proofEngine.cmo sequentPp.cmo xml2Gdome.cmo 
 gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx mquery.cmx \
diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index 781704b65..a8f9d6b06 100644
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -1,6 +1,6 @@
 BIN_DIR = /usr/local/bin
 REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \
-           helm-xml gdome2-xslt helm-cic_unification
+           helm-xml gdome2-xslt helm-cic_unification helm-mathql_interpreter
 PREDICATES =
 OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
 OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
@@ -14,11 +14,12 @@ all: gTopLevel
 opt: gTopLevel.opt
 
 DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml cic2Xml.ml \
-          cic2acic.ml logicalOperations.ml sequentPp.ml mathql.ml mquery.mli mquery.ml gTopLevel.ml
+          cic2acic.ml logicalOperations.ml sequentPp.ml mquery.mli mquery.ml \
+          gTopLevel.ml
 
 TOPLEVELOBJS = xml2Gdome.cmo proofEngineReduction.cmo proofEngine.cmo \
                cic2Xml.cmo cic2acic.cmo logicalOperations.cmo sequentPp.cmo \
-               mathql.cmo mquery.cmo gTopLevel.cmo
+               mquery.cmo gTopLevel.cmo
 
 depend:
 	$(OCAMLDEP) $(DEPOBJS) > .depend
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 1d5650b1c..083bbc7eb 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1378,6 +1378,8 @@ let initialize_everything () =
 
 let _ =
  CicCooking.init () ;
+ Mquery.init () ;
  ignore (GtkMain.Main.init ()) ;
- initialize_everything ()
+ initialize_everything () ;
+ Mquery.close ()
 ;;
diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml
index fb670923d..316588f2c 100644
--- a/helm/gTopLevel/mquery.ml
+++ b/helm/gTopLevel/mquery.ml
@@ -72,9 +72,9 @@ let con s = "<font color=\"red\">\"" ^ s ^ "\" </font>"
 
 let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"
 
-let nl () = "<br>"
+let nl = "<br>"
 
-let par () = "<p>"
+let par = "<p>"
 
 (* HTML representation of a query *)
 
@@ -151,8 +151,8 @@ let tref_uref (u, i) =
 
 let out_ie (r, b) =
    let pos = if b then "HEAD: " else "TAIL: " in
-   res (pos ^ str_uref r) ^ nl () ^
-   con (pos ^ str_tref (tref_uref r)) ^ nl ()
+   res (pos ^ str_uref r) ^ nl ^
+   con (pos ^ str_tref (tref_uref r)) ^ nl
 
 let rec out_il = function
    | []           -> ""
@@ -253,14 +253,27 @@ let locate s =
 			  )
 		)
       in
-      out_query query ^ nl ()
+       match Mqint.execute query with
+          MQStrUri l ->
+           out_query query ^ nl ^ "Result: " ^  nl ^
+            String.concat nl l ^ nl
+        | MQRefs _ -> assert false (*CSC: ????????????????????????????? *)
    in
    match Str.split (Str.regexp "[ \t]+") s with
       | [] -> ""
-      | head :: tail -> par () ^ locate_aux head 
+      | head :: tail -> par ^ locate_aux head 
+;;
 
 let backward t =
    let uil = inspect t in
    let til = List.map tie_uie uil in
    let query = MQList (build_inter 0 til) in
-   par () ^ out_query query ^ nl () (* par () ^ out_il uil ^ *)
+    match Mqint.execute query with
+       MQStrUri l ->
+        par ^ out_query query ^ nl ^ (* ^ par ^ out_il uil ^ *)
+        "Result: " ^  nl ^ String.concat nl l ^ nl
+     | MQRefs _ -> assert false (*CSC: ????????????????????????????? *)
+;;
+
+let init = Mqint.init;;
+let close = Mqint.close;;
diff --git a/helm/gTopLevel/mquery.mli b/helm/gTopLevel/mquery.mli
index d7889cb51..bfdf89597 100644
--- a/helm/gTopLevel/mquery.mli
+++ b/helm/gTopLevel/mquery.mli
@@ -43,3 +43,5 @@ val locate    : string -> string               (* LOCATE query building function
 
 val backward  : Cic.term -> string             (* BACKWARD query building function *)
 
+val init : unit -> unit
+val close : unit -> unit