Better handling of queries. Now both the locate and backward queries give

[helm.git] / helm / gTopLevel / mQueryGenerator.ml

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index bb27633bb5c4694d0cc69f4866cfb4e7b3b5bb32..eabc234aa16a7edc793986c0d62b7894e2a16206 100644 (file)
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -160,8 +160,8 @@ let build_result query =
    if ! issue query then
       let html = par () ^ out_query query ^ nl () in
       let result = Mqint.execute query in
-      save (html ^ out_result result)
-    else ""
+       result, save (html ^ out_result result)
+    else MQRefs [], ""
     
 let build_select (r, b, v) n  =
    let rvar = "ref" ^ string_of_int n in
@@ -220,8 +220,21 @@ let locate_query s =
                        )
              )
 
-let locate s = Mqint.execute (locate_query s)
-let locate_html s = build_result (locate_query s)
+let locate s =
+ let MQRefs uris, html = build_result (locate_query s) in
+(*CSC: here I am mapping .ind URIs to .ind#1/1, i.e. the first type of *)
+(*CSC: the mutual inductive block. It must be removed once the query   *)
+(*CSC: works reasonably.                                               *)
+  MQRefs (
+   List.map
+    (function uri ->
+      if String.sub uri (String.length uri - 4) 4 = ".ind" then
+       uri ^ "#1/1"
+      else
+       uri
+    ) uris
+  ), html
+;;
 
 let levels e c t =
    env := e; cont := c;
@@ -238,10 +251,11 @@ let backward e c t level =
    let query = build_inter 0 (il_restrict level il) in
    let query' = restrict_universe query il in
    let query'' = MQList query' in 
-   let r = build_result query'' in
-   if r <> "" then
+   let res = build_result query'' in
+   let r,html = res in
+   if html <> "" then
    begin
       print_endline ("GEN = " ^ string_of_int (List.length il) ^ ":" ^
          string_of_float (Sys.time () -. t0) ^ "s");
-      par () ^ il_out il ^ r
-   end else ""
+      r, par () ^ il_out il ^ html
+   end else res