]> matita.cs.unibo.it Git - helm.git/commitdiff
patches for the new interface of text_of_query/text_of result
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 3 Feb 2003 17:32:56 +0000 (17:32 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 3 Feb 2003 17:32:56 +0000 (17:32 +0000)
helm/gTopLevel/disambiguate.ml
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/mQueryGenerator.ml
helm/gTopLevel/topLevel/.depend
helm/gTopLevel/topLevel/Makefile
helm/gTopLevel/topLevel/topLevel.ml

index ff794fd5b2d03052bbea92803443159b059dda2e..2f02818474b5ccdd1e2f606dd0470817e85c2571 100644 (file)
 (******************************************************************************)
 
 (* 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 ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
+   out (!query ^ " <h1>Result:</h1> "); MQueryUtil.text_of_result out result "<br>";
+   !query
 ;;
 
 (** This module provides a functor to disambiguate the input **)
index c02711dd35afaa575e16dfe4ef20fe856381b696..c1dc822b68761242022f9df50932748ebe0952ca 100644 (file)
@@ -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 ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
+   (function q -> 
+    query := ""; MQueryUtil.text_of_query out q ""; true);
+  function result ->
+   out (!query ^ " <h1>Result:</h1> "); MQueryUtil.text_of_result out result "<br>";
+   !query
 ;;
 
 let
index 7e061eb0be302de929f024498d6d275f8edd13fb..ed52e55bda7e11825d8299628fcb2c6369d990c8 100644 (file)
@@ -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)
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..6ca33a924b85a649a29c06da6b6fb00ca03c3b45 100644 (file)
@@ -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 
index 24c631a1059413381ba9d132da87f71db548cd79..1245ae089062c60e7ec13eff3fc3e4aeb45ca652 100644 (file)
@@ -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))
index 338db29a7107a7ce8a15beb4be48ef2f843c682a..06ef93ab5f5571ec27a9455a2a7147c9773d7974 100644 (file)
@@ -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