X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FmQueryGenerator.ml;h=4deaf8c7a23d8923828a75977f35c9a36b394b31;hb=de211e50e79877a910eb85a63e47105108a7173d;hp=7dbf75262dd74bed7f4ab07f6b88d33d7a536e98;hpb=130b8e71a61cf5305894914c6f6431a9e924923c;p=helm.git

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 7dbf75262..4deaf8c7a 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
                           
@@ -169,7 +185,7 @@ let execute_query query =
 
 let locate s =
    let module M = MathQL in
-   let q = M.Ref (M.Fun "uri_of_alias" (M.Const [s])) in
+   let q = M.Ref (M.Fun "reference" (M.Const [s])) in
    execute_query q
 
 let backward e c t level =