]> matita.cs.unibo.it Git - helm.git/commitdiff
query numeration added
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 15 Oct 2002 16:00:21 +0000 (16:00 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 15 Oct 2002 16:00:21 +0000 (16:00 +0000)
helm/gTopLevel/mQueryGenerator.ml

index 7dbf75262dd74bed7f4ab07f6b88d33d7a536e98..6a1eb923d2eb6b50b3113d8c01d2192427b66eaa 100644 (file)
@@ -134,6 +134,8 @@ exception Discard
 
 let nl = " <p>\n"
 
+let query_num = ref 1
+
 let log_file = ref ""
 
 let confirm_query = ref (fun _ -> true)
@@ -152,16 +154,30 @@ let execute_query query =
    let module Util = MQueryUtil in
    let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
    let perm = 64 * 6 + 8 * 6 + 4 in
+   let time () =
+      let lt = Unix.localtime (Unix.time ()) in
+      "NEW LOG: " ^
+      string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
+      string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
+      string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
+      string_of_int (lt.Unix.tm_hour) ^ ":" ^
+      string_of_int (lt.Unix.tm_min) ^ ":" ^
+      string_of_int (lt.Unix.tm_sec) 
+   in
    let log q r = 
       let och = open_out_gen mode perm ! log_file in
-      let str = "Query:" ^ nl ^ Util.text_of_query q ^ nl ^ 
+      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; 
-      flush och
+      flush och 
    in
    let execute q =
       let r = Mqint.execute q in    
-      if ! log_file <> "" then log q r; r
+      if ! log_file <> "" then log q r; 
+      info := string_of_int ! query_num :: ! info;
+      incr query_num;
+      r
    in 
    if ! confirm_query query then execute query else raise Discard