connected instance to the web search engine

diff --git a/helm/searchEngine/html/moogle_form.html.src b/helm/searchEngine/html/moogle_form.html.src
index c594a10ffab17361278c6abba3a06d0bfe2d93bc..9bc072d360e7db2f2bc25648aa1baa72b3c95727 100644 (file)
--- a/helm/searchEngine/html/moogle_form.html.src
+++ b/helm/searchEngine/html/moogle_form.html.src
@@ -19,6 +19,7 @@
          <input type="submit" value="hint" name="param.action" />
          <input type="submit" value="match" name="param.action" />
          <input type="submit" value="elim" name="param.action" />
+         <input type="submit" value="instance" name="param.action" />
        </td>
        <td>&#xA0;&#xA0;&#xA0;</td>
        <td>

diff --git a/helm/searchEngine/html/moogle_init.html b/helm/searchEngine/html/moogle_init.html
index 7e35487f899702ddf78dd55540de27d4f339d304..7202e283d291d0fe6958f0150538e42b1c62bbbf 100644 (file)
--- a/helm/searchEngine/html/moogle_init.html
+++ b/helm/searchEngine/html/moogle_init.html
@@ -74,6 +74,7 @@ onclick="submit_query('w')" />
   <input type="submit" value="hint" name="param.action" />
   <input type="submit" value="match" name="param.action" />
   <input type="submit" value="elim" name="param.action" />
+  <input type="submit" value="instance" name="param.action" />
   </td>
   <td valign="top" width="25%">
    <font size="-2">

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))