From 4afb38bb0927c06ab4e64656f31cfc0fcb089b1e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 20 May 2002 10:48:31 +0000 Subject: [PATCH] mquery.ml now really call the execution of the query. Locate and backward now really work!!! --- helm/gTopLevel/.depend | 4 ++-- helm/gTopLevel/Makefile | 7 ++++--- helm/gTopLevel/gTopLevel.ml | 4 +++- helm/gTopLevel/mquery.ml | 27 ++++++++++++++++++++------- helm/gTopLevel/mquery.mli | 2 ++ 5 files changed, 31 insertions(+), 13 deletions(-) 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 = "\"" ^ s ^ "\" " let res s = "\"" ^ s ^ "\" " -let nl () = "
" +let nl = "
" -let par () = "

" +let par = "

" (* 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 -- 2.39.2