From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 19 May 2005 10:05:45 +0000 (+0000)
Subject: connected instance to the web search engine
X-Git-Tag: single_binding~36
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c0cd1db2993db9e7daadde2aba399bebacc0ac2b;p=helm.git

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 c594a10ff..9bc072d36 100644
--- 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 7e35487f8..7202e283d 100644
--- 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 47ca04deb..655235c1e 100644
--- 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))