From ebc089606ccbb3e9dbde142542a1f98f5020b4dd Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
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
+    "<div class='resultsbar'>
+      <table width='100%%'>
+       <tr>
+        <td class='left'><b class='query_kind'>%s</b></td>
+        <td class='right'>%s</td>
+       </tr>
+      </table>
+     </div>
+     <br />
+     <div>
+     %s
+     </div>"
+     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
-    "<div class='resultsbar'>
-      <table width='100%%'>
-       <tr>
-        <td class='left'><b class='query_kind'>%s</b></td>
-        <td class='right'><b>%d</b> result%s found</td>
-       </tr>
-      </table>
-     </div>
-     <br />
-     <div>
-      <table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">%s</table>
-     </div>"
-    (query_of_req req)
-    results_no (if results_no > 1 then "s" else "") results
+   template query_kind
+    (sprintf "<b>%d</b> result%s found"
+      results_no (if results_no > 1 then "s" else ""))
+    (sprintf
+      "<table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">
+        %s
+       </table>"
+       results)
   else
-    "<div class='resultsbar'>no results found</div>"
+    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
 	 ("<html><body><ul>" ^
-	  String.concat "" (List.map (fun k,v -> "<li><key>" ^ k ^ "</key> = <value>" ^ v  ^ "</value></li>") res) ^
+	  String.concat "" (List.map (fun (k,v) -> "<li><key>" ^ k ^ "</key> = <value>" ^ v  ^ "</value></li>") res) ^
 	  "</ul></body></html>") outchan
     | "/setparams" ->
 	let serialized_param_value_list = serialize_param_list req#params in
-- 
2.39.2