From: Stefano Zacchiroli Date: Tue, 21 Dec 2004 17:19:40 +0000 (+0000) Subject: added URI printing in the result page (so that mouse-over is not the X-Git-Tag: V_0_1_0~157 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8ad6f4591d80a263510d516f4b5bc0d75aabd81c;p=helm.git added URI printing in the result page (so that mouse-over is not the only way to know the URI of results!) --- diff --git a/helm/searchEngine/html/moogle.html b/helm/searchEngine/html/moogle.html index 3c76f8b85..a128cef49 100644 --- a/helm/searchEngine/html/moogle.html +++ b/helm/searchEngine/html/moogle.html @@ -22,6 +22,7 @@ b.error { color: red } b.query_kind { font-size: large } body { font-family: sans-serif } + span.uri { color: blue; } diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml index 998274e08..dd3b63ded 100644 --- a/helm/searchEngine/mooglePp.ml +++ b/helm/searchEngine/mooglePp.ml @@ -59,9 +59,13 @@ let theory_of_result (req: Http_types.request) page result = sprintf " %d. + %s + + + %s" - !idx uri mode i) + !idx uri uri mode i) result "" in template query_kind