X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fmquery.ml;h=316588f2c9d2787f52edd5ea3d5eb1bdd0d22b63;hb=4afb38bb0927c06ab4e64656f31cfc0fcb089b1e;hp=fb670923d4ab75a5f742dd94daaadcf625bddb5d;hpb=1808f15362ca07bb4ad5b6802afbf6789683f0bd;p=helm.git

diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml
index fb670923d..316588f2c 100644
--- a/helm/gTopLevel/mquery.ml
+++ b/helm/gTopLevel/mquery.ml
@@ -72,9 +72,9 @@ let con s = "<font color=\"red\">\"" ^ s ^ "\" </font>"
 
 let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"
 
-let nl () = "<br>"
+let nl = "<br>"
 
-let par () = "<p>"
+let par = "<p>"
 
 (* HTML representation of a query *)
 
@@ -151,8 +151,8 @@ let tref_uref (u, i) =
 
 let out_ie (r, b) =
    let pos = if b then "HEAD: " else "TAIL: " in
-   res (pos ^ str_uref r) ^ nl () ^
-   con (pos ^ str_tref (tref_uref r)) ^ nl ()
+   res (pos ^ str_uref r) ^ nl ^
+   con (pos ^ str_tref (tref_uref r)) ^ nl
 
 let rec out_il = function
    | []           -> ""
@@ -253,14 +253,27 @@ let locate s =
 			  )
 		)
       in
-      out_query query ^ nl ()
+       match Mqint.execute query with
+          MQStrUri l ->
+           out_query query ^ nl ^ "Result: " ^  nl ^
+            String.concat nl l ^ nl
+        | MQRefs _ -> assert false (*CSC: ????????????????????????????? *)
    in
    match Str.split (Str.regexp "[ \t]+") s with
       | [] -> ""
-      | head :: tail -> par () ^ locate_aux head 
+      | head :: tail -> par ^ locate_aux head 
+;;
 
 let backward t =
    let uil = inspect t in
    let til = List.map tie_uie uil in
    let query = MQList (build_inter 0 til) in
-   par () ^ out_query query ^ nl () (* par () ^ out_il uil ^ *)
+    match Mqint.execute query with
+       MQStrUri l ->
+        par ^ out_query query ^ nl ^ (* ^ par ^ out_il uil ^ *)
+        "Result: " ^  nl ^ String.concat nl l ^ nl
+     | MQRefs _ -> assert false (*CSC: ????????????????????????????? *)
+;;
+
+let init = Mqint.init;;
+let close = Mqint.close;;