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 e2b5d773003abf08d286808c584d65c3b051b469..63ec81c6c12fa008e8b07f10c73a66600f28775d 100644 (file)
--- 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 781704b65dbc0f2d418a60d6f45bcfe2be5ab017..a8f9d6b06709222bac1ebb70eeb97045b5250e65 100644 (file)
--- 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 1d5650b1ca20670fdad520c77412c6a1bd924842..083bbc7ebac6ccfc279d69cd00911210519ae7c6 100644 (file)
--- 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 fb670923d4ab75a5f742dd94daaadcf625bddb5d..316588f2c9d2787f52edd5ea3d5eb1bdd0d22b63 100644 (file)
--- 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 d7889cb517694947c7b510af63309718bfcd93f2..bfdf89597e4c43cb910f46d7a2bd2fe83aa05284 100644 (file)
--- 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