X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=a140666aca5d3d2434f78bcd6d3bac75592ed246;hb=d3c72d6856cd185e5b3e9f2e8b928b78c7031ed1;hp=622f10bd5a618979fcf19551b1c32a659536cd99;hpb=506b4b7597021c98e34fb65cf9d0bb7879f06e92;p=helm.git

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 622f10bd5..a140666ac 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -178,20 +178,20 @@ let contype = "Content-Type", "text/html";;
 let get_constraints term =
  function
     | "/locateInductivePrinciple" ->
-      CGLocateInductive.universe,
+      None,
       (CGLocateInductive.get_constraints term),
       (None,None,None)
     | "/searchPattern" ->
      let constr_obj, constr_rel, constr_sort =
        CGSearchPattern.get_constraints term in
-      CGSearchPattern.universe,
-       (constr_obj, constr_rel, constr_sort),
-       (Some constr_obj, Some constr_rel, Some constr_sort)
+     (Some CGSearchPattern.universe),
+     (constr_obj, constr_rel, constr_sort),
+     (Some constr_obj, Some constr_rel, Some constr_sort)
     | "/matchConclusion" ->
      let list_of_must, only = CGMatchConclusion.get_constraints [] [] term in
 (* FG: there is no way to choose the block number ***************************)
      let block = pred (List.length list_of_must) in 
-      CGMatchConclusion.universe, 
+      (Some CGMatchConclusion.universe), 
       (List.nth list_of_must block, [], []), (Some only, None, None)
     | _ -> assert false
 ;;
@@ -345,7 +345,7 @@ let callback (req: Http_types.request) outchan =
       if List.mem server_and_port valid_servers then
         Http_daemon.respond
           ~headers:["Content-Type", "text/html"]
-          ~body:(Http_client.Convenience.http_get url)
+          ~body:(Http_client.http_get url)
           outchan
       else
         Http_daemon.respond
@@ -413,7 +413,16 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
             let set_metasenv metasenv =
               CicTextualParser0.metasenv := metasenv
 
-            let output_html = prerr_endline
+            let output_html ?(append_NL = true) html_msg =
+              let rec collect_string = function
+                | `BR -> "\n"
+                | `T s -> s
+                | `L tags -> String.concat "" (List.map collect_string tags)
+              in
+              match html_msg with
+              | `Error msg | `Msg msg ->
+                  (if append_NL then prerr_endline else prerr_string)
+                    (collect_string msg ^ (if append_NL then "\n" else ""))
 
             let interactive_user_uri_choice
               ~selection_mode ?ok
@@ -426,7 +435,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
                   let msg = Pcre.replace ~pat:"\'" ~templ:"\\\'" msg in
                   (match selection_mode with
                   | `SINGLE -> assert false
-                  | `EXTENDED ->
+                  | `MULTIPLE ->
                       Http_daemon.send_basic_headers ~code:200 outchan ;
                       Http_daemon.send_CRLF outchan ;
                       iter_file
@@ -579,7 +588,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
                   raise Chat_unfinished)
             in
             let query =
-             G.query_of_constraints (Some universe) must'' only'
+             G.query_of_constraints universe must'' only'
             in
 	          let results = MQueryInterpreter.execute mqi_handle query in 
              Http_daemon.send_basic_headers ~code:200 outchan ;