]> matita.cs.unibo.it Git - helm.git/commitdiff
some interfaces changed to prepare the mathql code for version 1.4
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 29 Oct 2003 15:40:25 +0000 (15:40 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 29 Oct 2003 15:40:25 +0000 (15:40 +0000)
helm/Makefile
helm/gTopLevel/.depend
helm/gTopLevel/disambiguate.ml
helm/gTopLevel/gTopLevel.ml
helm/mathql_test/mqgtop.ml
helm/mathql_test/mqtop.ml
helm/ocaml/mathql_interpreter/.depend
helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
helm/ocaml/mathql_interpreter/mQueryUtil.ml
helm/ocaml/mathql_interpreter/mQueryUtil.mli
helm/searchEngine/searchEngine.ml

index 721a8962121a6593e450a009b785fad81e5ea0a8..0b925d51504ec6fd25ef2a2f91da8aa2e98dda40 100644 (file)
@@ -1,4 +1,5 @@
-DIRS = ocaml hbugs gTopLevel searchEngine mathql_test
+DIRS = ocaml gTopLevel searchEngine mathql_test
+# hbugs
 
 DIRS_BYTE = $(patsubst %,%.byte,$(DIRS))
 DIRS_OPT = $(patsubst %,%.opt,$(DIRS))
index af62a9fcb23a51fb8520872784b7299ef4f90f1a..6da67a4a543564085fbe41e7a48949017e375064 100644 (file)
@@ -1,3 +1,6 @@
+termEditor.cmi: disambiguate.cmi 
+texTermEditor.cmi: disambiguate.cmi 
+invokeTactics.cmi: termEditor.cmi termViewer.cmi 
 proofEngine.cmo: proofEngine.cmi 
 proofEngine.cmx: proofEngine.cmi 
 logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi 
@@ -6,10 +9,8 @@ disambiguate.cmo: disambiguate.cmi
 disambiguate.cmx: disambiguate.cmi 
 termEditor.cmo: disambiguate.cmi termEditor.cmi 
 termEditor.cmx: disambiguate.cmx termEditor.cmi 
-termEditor.cmi: disambiguate.cmi 
 texTermEditor.cmo: disambiguate.cmi texTermEditor.cmi 
 texTermEditor.cmx: disambiguate.cmx texTermEditor.cmi 
-texTermEditor.cmi: disambiguate.cmi 
 xmlDiff.cmo: xmlDiff.cmi 
 xmlDiff.cmx: xmlDiff.cmi 
 termViewer.cmo: logicalOperations.cmi xmlDiff.cmi termViewer.cmi 
@@ -18,11 +19,7 @@ invokeTactics.cmo: logicalOperations.cmi proofEngine.cmi termEditor.cmi \
     termViewer.cmi invokeTactics.cmi 
 invokeTactics.cmx: logicalOperations.cmx proofEngine.cmx termEditor.cmx \
     termViewer.cmx invokeTactics.cmi 
-invokeTactics.cmi: termEditor.cmi termViewer.cmi 
-hbugs.cmo: invokeTactics.cmi proofEngine.cmi hbugs.cmi 
-hbugs.cmx: invokeTactics.cmx proofEngine.cmx hbugs.cmi 
-hbugs.cmi: invokeTactics.cmi 
-gTopLevel.cmo: hbugs.cmi invokeTactics.cmi logicalOperations.cmi \
-    proofEngine.cmi termEditor.cmi termViewer.cmi texTermEditor.cmi 
-gTopLevel.cmx: hbugs.cmx invokeTactics.cmx logicalOperations.cmx \
-    proofEngine.cmx termEditor.cmx termViewer.cmx texTermEditor.cmx 
+gTopLevel.cmo: invokeTactics.cmi logicalOperations.cmi proofEngine.cmi \
+    termEditor.cmi termViewer.cmi texTermEditor.cmi 
+gTopLevel.cmx: invokeTactics.cmx logicalOperations.cmx proofEngine.cmx \
+    termEditor.cmx termViewer.cmx texTermEditor.cmx 
index 974e0b49e6655492aa4dd7a97b1c8b5043275b89..efb1c05081d06cd16f1f748e72cfc2be8d21b7f8 100644 (file)
@@ -73,9 +73,9 @@ module Make(C:Callbacks) =
         MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
       ) result in
      C.output_html "<h1>Locate Query: </h1><pre>";
-     MQueryUtil.text_of_query C.output_html query ""
+     MQueryUtil.text_of_query C.output_html "" query
      C.output_html "<h1>Result:</h1>";
-     MQueryUtil.text_of_result C.output_html result "<br>";
+     MQueryUtil.text_of_result C.output_html "<br>" result;
      let uris' =
       match uris with
          [] ->
index 7861304ef1f6a2f7c6abc5195a49a1c8f36906b7..9fd0b352b838bfb14b9b28887b58eb266a81c8e7 100644 (file)
@@ -982,9 +982,9 @@ let locate_callback id =
      MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
    result in
   out "<h1>Locate Query: </h1><pre>";
-  MQueryUtil.text_of_query out query ""
+  MQueryUtil.text_of_query out "" query
   out "<h1>Result:</h1>";
-  MQueryUtil.text_of_result out result "<br>";
+  MQueryUtil.text_of_result out "<br>" result;
   user_uri_choice ~title:"Ambiguous input."
    ~msg:
      ("Ambiguous input \"" ^ id ^
index edf714b1e6a1ecb0e6f2216079182d68d84a6617..d13ab253842c66fa87eef8d88130159e1f268ad4 100644 (file)
@@ -73,14 +73,14 @@ let issue handle q =
       let out = output_string och in 
       if ! query_num = 1 then out (time () ^ nl);
       out ("Query: " ^ string_of_int ! query_num ^ nl);
-      U.text_of_query out q nl;
+      U.text_of_query out nl q;
       out ("Result: " ^ nl);
-      U.text_of_result out r nl;
+      U.text_of_result out nl r;
       close_out och
    in
-   if ! show_queries then U.text_of_query (output_string stdout) q nl;
+   if ! show_queries then U.text_of_query (output_string stdout) nl q;
    let r = I.execute handle q in    
-   U.text_of_result (output_string stdout) r nl;
+   U.text_of_result (output_string stdout) nl r;
    if ! log_file <> "" then log q r; 
    incr query_num;
    flush stdout
index 48ffb1e74078f227a3b78e582822fb8ffda168e5..851a633911b4cf5d4b25e84fe39e1531a2987238 100644 (file)
@@ -32,7 +32,7 @@ let _ =
    let ich = Lexing.from_channel stdin in
    let rec aux () =
       let t = U.start_time () in
-      U.text_of_query print_string (U.query_of_text ich) "\n";
+      U.text_of_query print_string "\n" (U.query_of_text ich);
       Printf.printf "mqtop: query: %s\n" (U.stop_time t);
       flush stdout; aux()
    in
index 7d9b3c6257f0e968ea03155348276c90fbf448f7..bbe2948d5e3cedf4862fdb5811b0ac9f8c186900 100644 (file)
@@ -1,11 +1,9 @@
 mQIConn.cmi: mQIMap.cmi 
 mQIProperty.cmi: mQIConn.cmi 
 mQueryInterpreter.cmi: mQIConn.cmi 
-mQueryTParser.cmo: mQueryTParser.cmi 
-mQueryTParser.cmx: mQueryTParser.cmi 
-mQueryTLexer.cmo: mQueryTParser.cmi 
+mQueryTLexer.cmo: mQueryTParser.cmo 
 mQueryTLexer.cmx: mQueryTParser.cmx 
-mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmi mQueryUtil.cmi 
+mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmo mQueryUtil.cmi 
 mQueryUtil.cmx: mQueryTLexer.cmx mQueryTParser.cmx mQueryUtil.cmi 
 mQIUtil.cmo: mQIUtil.cmi 
 mQIUtil.cmx: mQIUtil.cmi 
index b2bfd445dd59ae71d247bcea7b6800a7a6d90c42..a5adbcd393ceaf14a0bb2be8460083bbc1873d49 100644 (file)
@@ -56,7 +56,7 @@ let execute h x =
      if C.set h C.Warn then 
      begin
         C.log h "MQIExecute: waring: reference to undefined variables: ";
-       P.text_of_query (C.log h) q "\n"
+       P.text_of_query (C.log h) "\n" q
      end
    in
    let rec eval_val c = function
@@ -131,7 +131,7 @@ let execute h x =
       | M.Log (_,b,x) ->
          if b then begin
            let t = P.start_time () in
-           P.text_of_query (C.log h) x "\n";
+           P.text_of_query (C.log h) "\n" x;
            let s = P.stop_time t in
            if C.set h C.Stat then 
               C.log h (Printf.sprintf "Log source: %s\n" s);
@@ -139,7 +139,7 @@ let execute h x =
         end else begin
             let s = (eval_query c x) in
            let t = P.start_time () in
-           P.text_of_result (C.log h) s "\n"
+           P.text_of_result (C.log h) "\n" s
            let r = P.stop_time t in
            if C.set h C.Stat then 
               C.log h (Printf.sprintf "Log: %s\n" r);
index 4484c486b181e89d9c734be408f1f67f7f80b1d4..e8344b0d60daa3fdb3c94bc833c1d220ba4a2296 100644 (file)
@@ -37,7 +37,7 @@ let txt_str out s = out ("\"" ^ s ^ "\"")
 
 let txt_path out p = out "/"; txt_list out (txt_str out) "/" p 
 
-let text_of_query out x sep =
+let text_of_query out sep x =
    let module M = MathQL in 
    let txt_path_list l = txt_list out (txt_path out) ", " l in 
    let txt_svar sv = out ("%" ^ sv) in 
@@ -155,7 +155,7 @@ let text_of_query out x sep =
    in 
    txt_set x; out sep
 
-let text_of_result out x sep = 
+let text_of_result out sep x = 
    let txt_attr = function
       | (p, []) -> txt_path out p
       | (p, l)  -> txt_path out p; out " = "; txt_list out (txt_str out) ", " l
index 2a3c80b839695f58a889c92f5a0765bda6a5da6a..5754002980b8e6e68fa575e4de9d41f4824bfef0 100644 (file)
@@ -26,9 +26,9 @@
 (*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
  *)
 
-val text_of_query  : (string -> unit) -> MathQL.query -> string -> unit
+val text_of_query  : (string -> unit) -> string -> MathQL.query -> unit
 
-val text_of_result : (string -> unit) -> MathQL.result -> string -> unit
+val text_of_result : (string -> unit) -> string -> MathQL.result -> unit
 
 val query_of_text  : Lexing.lexbuf -> MathQL.query
 
index f7fae9481e6d0ac093705fa5fd21f7f50fba5dd7..535b5f83f398408ac3bca5b534eeaa3e9e921c1a 100644 (file)
@@ -426,7 +426,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
                   let msg = Pcre.replace ~pat:"\'" ~templ:"\\\'" msg in
                   (match selection_mode with
                   | `SINGLE -> assert false
-                  | `EXTENDED ->
+                  | `MULTIPLE ->
                       Http_daemon.send_basic_headers ~code:200 outchan ;
                       Http_daemon.send_CRLF outchan ;
                       iter_file