From a3ef256812f0397a871fe8e69c125dfd89e62dce Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 3 Feb 2003 17:32:56 +0000 Subject: [PATCH] patches for the new interface of text_of_query/text_of result --- helm/gTopLevel/disambiguate.ml | 8 ++++++-- helm/gTopLevel/gTopLevel.ml | 9 +++++++-- helm/gTopLevel/mQueryGenerator.ml | 11 +++++------ helm/gTopLevel/topLevel/.depend | 4 ++++ helm/gTopLevel/topLevel/Makefile | 2 +- helm/gTopLevel/topLevel/topLevel.ml | 8 ++++---- 6 files changed, 27 insertions(+), 15 deletions(-) diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml index ff794fd5b..2f0281847 100644 --- a/helm/gTopLevel/disambiguate.ml +++ b/helm/gTopLevel/disambiguate.ml @@ -34,12 +34,16 @@ (******************************************************************************) (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *) +(* FG : THIS FUNCTION IS BECOMING A REAL NONSENSE *) let get_last_query = let query = ref "" in + let out s = query := ! query ^ s in MQueryGenerator.set_confirm_query - (function q -> query := MQueryUtil.text_of_query q ; true) ; + (function q -> + query := ""; MQueryUtil.text_of_query out q ""; true); function result -> - !query ^ "

Result:

" ^ MQueryUtil.text_of_result result "
" + out (!query ^ "

Result:

"); MQueryUtil.text_of_result out result "
"; + !query ;; (** This module provides a functor to disambiguate the input **) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index c02711dd3..c1dc822b6 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -383,11 +383,16 @@ let interactive_interpretation_choice interpretations = (* MISC FUNCTIONS *) (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *) +(* FG : THIS FUNCTION IS BECOMING A REAL NONSENSE *) let get_last_query = let query = ref "" in + let out s = query := ! query ^ s in MQueryGenerator.set_confirm_query - (function q -> query := MQueryUtil.text_of_query q ; true) ; - function result -> !query ^ "

Result:

" ^ MQueryUtil.text_of_result result "
" + (function q -> + query := ""; MQueryUtil.text_of_query out q ""; true); + function result -> + out (!query ^ "

Result:

"); MQueryUtil.text_of_result out result "
"; + !query ;; let diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml index 7e061eb0b..ed52e55bd 100644 --- a/helm/gTopLevel/mQueryGenerator.ml +++ b/helm/gTopLevel/mQueryGenerator.ml @@ -86,11 +86,10 @@ let execute_query query = in let log q r = let och = open_out_gen mode perm ! log_file in - if ! query_num = 1 then output_string och (time () ^ nl); - let str = - "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^ - "Result:" ^ nl ^ Util.text_of_result r nl in - output_string och str; + let out = output_string och in + if ! query_num = 1 then out (time () ^ nl); + out ("Query: " ^ string_of_int ! query_num ^ nl); Util.text_of_query out q nl; + out ("Result:" ^ nl); Util.text_of_result out r nl; flush och in let execute q = @@ -551,5 +550,5 @@ let searchPattern must_use can_use = (*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*) -print_endline ("### " ^ MQueryUtil.text_of_query (q_let_po opos 1)) ; flush stdout; +print_endline "### "; MQueryUtil.text_of_query print_string (q_let_po opos 1) "\n"; flush stdout; execute_query (q_let_po opos 1) diff --git a/helm/gTopLevel/topLevel/.depend b/helm/gTopLevel/topLevel/.depend index e69de29bb..6ca33a924 100644 --- a/helm/gTopLevel/topLevel/.depend +++ b/helm/gTopLevel/topLevel/.depend @@ -0,0 +1,4 @@ +topLevel.cmo: ../mQueryGenerator.cmi ../../ocaml/mathql/mQueryUtil.cmi \ + ../../ocaml/mathql_interpreter/mqint.cmi +topLevel.cmx: ../mQueryGenerator.cmx ../../ocaml/mathql/mQueryUtil.cmx \ + ../../ocaml/mathql_interpreter/mqint.cmx diff --git a/helm/gTopLevel/topLevel/Makefile b/helm/gTopLevel/topLevel/Makefile index 24c631a10..1245ae089 100644 --- a/helm/gTopLevel/topLevel/Makefile +++ b/helm/gTopLevel/topLevel/Makefile @@ -4,7 +4,7 @@ PREDICATES = OCAMLOPTIONS = -I .. -package "$(REQUIRES)" -predicates "$(PREDICATES)" OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) -OCAMLDEP = ocamldep +OCAMLDEP = ocamldep -I .. -I ../../ocaml/mathql_interpreter -I ../../ocaml/mathql LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml index 338db29a7..06ef93ab5 100644 --- a/helm/gTopLevel/topLevel/topLevel.ml +++ b/helm/gTopLevel/topLevel/topLevel.ml @@ -16,7 +16,7 @@ let check_db () = let default_confirm q = let module Util = MQueryUtil in - if ! show_queries then print_string (Util.text_of_query q ^ nl); + if ! show_queries then Util.text_of_query print_string q nl; let b = check_db () in if ! db_down then print_endline "db_down"; b @@ -79,7 +79,7 @@ let execute ich = Gen.set_confirm_query default_confirm; try let q = Util.query_of_text (Lexing.from_channel ich) in - print_endline (Util.text_of_result (Gen.execute_query q) nl); + Util.text_of_result print_string (Gen.execute_query q) nl; flush stdout with Gen.Discard -> () @@ -88,7 +88,7 @@ let locate name = let module Gen = MQueryGenerator in Gen.set_confirm_query default_confirm; try - print_endline (Util.text_of_result (Gen.locate name) nl); + Util.text_of_result print_string (Gen.locate name) nl; flush stdout with Gen.Discard -> () @@ -125,7 +125,7 @@ let mbackward n m l = let gen = List.nth info 1 in if Mqint.get_stat () then print_string (num ^ " GEN = " ^ gen ^ ":" ^ string_of_float t1 ^ "s" ^ nl); - print_string (Util.text_of_result r nl); + Util.text_of_result print_string r nl; flush stdout with Gen.Discard -> () in -- 2.39.2