From ebc089606ccbb3e9dbde142542a1f98f5020b4dd Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 20 Sep 2004 15:47:00 +0000 Subject: [PATCH] fixed parse error for ocaml 3.08 --- helm/searchEngine/searchEngine.ml | 65 ++++++++++++++++++++++--------- helm/uwobo/uwobo.ml | 2 +- 2 files changed, 47 insertions(+), 20 deletions(-) diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 1f45fe67c..1c58e5d29 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -47,6 +47,9 @@ let string_tail s = let _ = let configuration_file = "/projects/helm/etc/searchEngine.conf.xml" in Helm_registry.load_from configuration_file +let max_results_no = + Helm_registry.get_opt_default Helm_registry.get_int 10 + "search_engine.max_results_no" let port = Helm_registry.get_int "search_engine.port" @@ -124,8 +127,25 @@ let query_of_req (req: Http_types.request) = (** pretty print a MathQL query result to an HELM theory file *) let theory_of_result req result = let results_no = List.length result in + let query_kind = query_of_req req in + let template query_kind summary results = + sprintf + "
+ + + + + +
%s%s
+
+
+
+ %s +
" + query_kind summary results + in if results_no > 0 then - let mode = if results_no > 10 then "linkonly" else "typeonly" in + let mode = if results_no > max_results_no then "linkonly" else "typeonly" in let results = let idx = ref (results_no + 1) in List.fold_right @@ -139,23 +159,16 @@ let theory_of_result req result = !idx uri mode i) result "" in - sprintf - "
- - - - - -
%s%d result%s found
-
-
-
- %s
-
" - (query_of_req req) - results_no (if results_no > 1 then "s" else "") results + template query_kind + (sprintf "%d result%s found" + results_no (if results_no > 1 then "s" else "")) + (sprintf + " + %s +
" + results) else - "
no results found
" + template query_kind "no results found" "" let pp_result req result = sprintf @@ -332,7 +345,7 @@ let send_results results let key' = (Pcre.extract ~pat:"param\\.(.*)" key).(1) in Pcre.regexp ("@" ^ key' ^ "@"), value) (List.filter - (fun (key,_) as p-> Pcre.pmatch ~pat:"^param\\." key) + (fun ((key,_) as p) -> Pcre.pmatch ~pat:"^param\\." key) req#params)) @ (if req#param "advanced" = "no" then [ simple_checked_RE, "checked='true'"; @@ -514,7 +527,21 @@ let exec_action mqi_handle (req: Http_types.request) outchan = | MQIConn.MySQL_C conn -> conn | _ -> assert false in +(* + (* ZACK: constraints sulla conclusione, no apply *) let results = List.map snd (Match_concl.cmatch dbd term') in +*) + (* ZACK: constraints sulle costanti + apply *) + let status = ProofEngineTypes.initial_status term' [] in + let intros = PrimitiveTactics.intros_tac () in + let subgoals = ProofEngineTypes.apply_tactic intros status in + let results = + match subgoals with + | proof, [goal] -> + let (uri,metasenv,bo,ty) = proof in + TacticChaser.searchTheorems_for_hint mqi_handle (proof, goal) + | _ -> assert false + in send_results (`Results results) ~id_to_uris:id_to_uris' req outchan else let must'', only' = @@ -717,7 +744,7 @@ let callback mqi_handle (req: Http_types.request) outchan = Pcre.regexp ("@" ^ key' ^ "@"), value ) (List.filter - (fun (key,_) as p-> Pcre.pmatch ~pat:"^param\\." key) + (fun ((key,_) as p) -> Pcre.pmatch ~pat:"^param\\." key) req#params) )) line) ^ diff --git a/helm/uwobo/uwobo.ml b/helm/uwobo/uwobo.ml index 345ccda59..4154dfb3d 100644 --- a/helm/uwobo/uwobo.ml +++ b/helm/uwobo/uwobo.ml @@ -442,7 +442,7 @@ let callback let res = Uwobo_profiles.get_params pid ?password () in respond_html ("") outchan | "/setparams" -> let serialized_param_value_list = serialize_param_list req#params in -- 2.39.2