From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 15 Oct 2002 16:00:21 +0000 (+0000)
Subject: query numeration added
X-Git-Tag: new_mathql_before_first_merge~4
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a30cfd97783975d44953df4b9a3c47a327d71724;p=helm.git

query numeration added
---

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 7dbf75262..6a1eb923d 100644
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -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