From: Stefano Zacchiroli 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 @@ +     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')" /> + 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))