X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FmQueryGenerator.ml;h=4deaf8c7a23d8923828a75977f35c9a36b394b31;hb=6cd9c31edf69f619789a9802e840fbb61f4b6b40;hp=429d445f7ced89fbd8af701f9159c22fc419cecf;hpb=ea6cbd87e90a25321951219d0fb47c256c464540;p=helm.git

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 429d445f7..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 =
@@ -178,7 +194,7 @@ let backward e c t level =
    let q_where = M.Sub (M.RefOf (
       M.Select ("uri", 
                 M.Relation (M.ExactOp, ["refObj"], M.RVar "uri0", ["pos"]),
-                M.Ex (M.Meet (M.VVar "positions", M.Record ("uri", "pos")))
+                M.Ex ["uri"] (M.Meet (M.VVar "positions", M.Record ("uri", "pos"))) 
 	       )),      M.VVar "universe"
 		       )
    in
@@ -193,7 +209,7 @@ let backward e c t level =
       let pos = if b then "MainConclusion" else "InConclusion" in
       M.Select ("uri", 
                 M.Relation (M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]),
-                M.Ex (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
+                M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
                )
    in 
    let rec build_intersect = function