X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=e52d0aa35da4d3f15ed5275f0f0bdc77ff86a9d2;hb=0d750a87e8b3f26964fc5a05cf559d86c913d962;hp=4c9f34989c223758ed245f7d4170441c0976a18d;hpb=13d18f963d7342cfeddf17f3ae222ff1b14404a8;p=helm.git

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 4c9f34989..e52d0aa35 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -45,7 +45,7 @@ let string_tail s =
 
   (* First of all we load the configuration *)
 let _ =
- let configuration_file = "searchEngine.conf.xml" in
+ let configuration_file = "/projects/helm/etc/searchEngine.conf.xml" in
   Helm_registry.load_from configuration_file
 ;;
 
@@ -130,7 +130,7 @@ let theory_of_result result =
    let results =
     let idx = ref (results_no + 1) in
      List.fold_right
-      (fun (uri,attrs) i ->
+      (fun uri i ->
         decr idx ;
         "<tr><td valign=\"top\">" ^ string_of_int !idx ^ ".</td><td><ht:OBJECT uri=\"" ^ uri ^ "\" mode=\"" ^ mode ^ "\"/></td></tr>" ^  i
       ) result ""
@@ -471,6 +471,19 @@ let exec_action mqi_handle (req: Http_types.request) outchan =
   ((only_obj, only_rel, only_sort) as only) =
     get_constraints term' req#path
   in
+  if
+    (try ignore (req#param "constraints"); false
+    with Http_types.Param_not_found _ -> true) &&
+    (req#param "advanced" = "no") && (req#path = "/hint")
+  then
+    let dbd =
+      match mqi_handle.MQIConn.pgc with
+      |   MQIConn.MySQL_C conn -> conn
+      | _ -> assert false
+    in
+    let results = List.map snd (Match_concl.cmatch dbd term') in
+    send_results results ~id_to_uris:id_to_uris' req outchan
+  else
   let must'', only' =
     (try
        add_user_constraints
@@ -555,7 +568,7 @@ let exec_action mqi_handle (req: Http_types.request) outchan =
     G.query_of_constraints universe must'' only'
   in
   let results = MQueryInterpreter.execute mqi_handle query in 
-  send_results results ~id_to_uris:id_to_uris' req outchan
+  send_results (List.map fst results) ~id_to_uris:id_to_uris' req outchan
 in
 
 (* HTTP DAEMON CALLBACK *)
@@ -625,13 +638,13 @@ let callback mqi_handle (req: Http_types.request) outchan =
             let query = G.locate expression in
              MQueryInterpreter.execute mqi_handle query
           in
-          send_results results req outchan
+          send_results (List.map fst results) req outchan
     | "/execute" ->
         let query_string = req#param "query" in
         let lexbuf = Lexing.from_string query_string in
         let query = MQueryUtil.query_of_text lexbuf in
         let result = MQueryInterpreter.execute mqi_handle query in
-        let result_string = pp_result result in
+        let result_string = pp_result (List.map fst result) in
         Http_daemon.respond ~body:result_string ~headers:[contype] outchan
 (*  Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan *)
     | "/unreferred" ->
@@ -639,7 +652,8 @@ let callback mqi_handle (req: Http_types.request) outchan =
         let source = req#param "source" in
         let query = G.unreferred target source in
         let result = MQueryInterpreter.execute mqi_handle query in
-        Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
+        Http_daemon.respond ~headers:[contype]
+          ~body:(pp_result (List.map fst result)) outchan
     | "/getpage" ->
         (* TODO implement "is_permitted" *)
         let _ = prerr_endline