in the particular case of simple searches, Andrea atmost/atleast/exactly

technique is used

diff --git a/helm/searchEngine/Makefile b/helm/searchEngine/Makefile
index 809a5abf7f6283c3dfd18fa895825d08bdb2423a..519629b5490057442363c1f62194fc91eb4619c1 100644 (file)
--- a/helm/searchEngine/Makefile
+++ b/helm/searchEngine/Makefile
@@ -1,7 +1,7 @@
 REQUIRES = http helm-cic_textual_parser2 helm-cic_proof_checking \
            helm-xml gdome2-xslt helm-cic_unification helm-mathql \
            helm-mathql_interpreter helm-mathql_generator helm-logger \
-           helm-tex_cic_textual_parser
+           helm-tex_cic_textual_parser helm-tactics
 OCAMLOPTIONS = -thread -package "$(REQUIRES)" -pp camlp4o -I ../gTopLevel
 OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
 OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS)

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 4c9f34989c223758ed245f7d4170441c0976a18d..9c479f13b5436b36fe9bdd000e6e4aa38a801f29 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -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")
+  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