- some code patched

[helm.git] / helm / searchEngine / searchEngine.ml

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index bfff6fd67d5a1a477d9c0101bf805b0d67b3030e..fc0fb9cbee4ec2af67bb77d7f2b12ccfc1f269c2 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -273,6 +273,7 @@ let callback mqi_handle (req: Http_types.request) outchan =
   try
     debug_print (sprintf "Received request: %s" req#path);
     (match req#path with
+    | "/help" -> Http_daemon.respond ~body:"HELM Search Engine" outchan
     | "/execute" ->
         let query_string = req#param "query" in
         let lexbuf = Lexing.from_string query_string in
@@ -458,8 +459,8 @@ let callback mqi_handle (req: Http_types.request) outchan =
                   interactive_interpretation_choice_TPL;
                 raise Chat_unfinished
 
-            let input_or_locate_uri ~title =
-              UriManager.uri_of_string "cic:/Coq/Init/DataTypes/nat_ind.con"
+            let input_or_locate_uri ~title ?id () =
+             assert false
 
           end
         in