connected instance to the web search engine

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

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 47ca04debbacd9f30074584da5ff48f99418c78e..655235c1e538121ca0b72bc124a90bc47db2b139 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -126,6 +126,7 @@ let query_kind_of_req (req: Http_types.request) =
   | "/hint" -> "Hint"
   | "/locate" -> "Locate"
   | "/elim" -> "Elim"
+  | "/instance" -> "Instance"
   | _ -> ""
 
   (* given a uri with a query part in input try to find in it a string
@@ -332,6 +333,7 @@ let exec_action dbd (req: Http_types.request) outchan =
     let uris =
       match req#path with
       | "/match" -> MetadataQuery.match_term ~dbd term
+      | "/instance" -> MetadataQuery.instance ~dbd term
       | "/hint" ->
           let status = ProofEngineTypes.initial_status term metasenv in
           let intros = PrimitiveTactics.intros_tac () in
@@ -410,6 +412,7 @@ let callback dbd (req: Http_types.request) outchan =
         end
     | "/hint"
     | "/elim"
+    | "/instance"
     | "/match" -> exec_action dbd req outchan
     | invalid_request ->
         Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))