From: Stefano Zacchiroli Date: Wed, 16 Jun 2004 13:42:32 +0000 (+0000) Subject: in the particular case of simple searches, Andrea atmost/atleast/exactly X-Git-Tag: pre_subst_in_kernel~29 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a0f2a7d4b328e5a621a5d62f474e5d552587d72f;p=helm.git 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 809a5abf7..519629b54 100644 --- 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 4c9f34989..9c479f13b 100644 --- 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 ; "" ^ string_of_int !idx ^ "." ^ 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