]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: cbd78f4)
added URI printing in the result page (so that mouse-over is not the
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 21 Dec 2004 17:19:40 +0000 (17:19 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 21 Dec 2004 17:19:40 +0000 (17:19 +0000)
only way to know the URI of results!)

helm/searchEngine/html/moogle.html patch | blob | history
helm/searchEngine/mooglePp.ml patch | blob | history

diff --git a/helm/searchEngine/html/moogle.html b/helm/searchEngine/html/moogle.html
index 3c76f8b852ccf66be7acd05ed9a3fe28aaf403b5..a128cef492ecd1d48c8216de2d22847e7e6a4cd2 100644 (file)
--- 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; }
 </style>
 </head>
 <body bgcolor="#ffffff">
diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml
index 998274e08525e60bd7d38a297d210ea1ae419d87..dd3b63ded91ba40e5f8d436a519b26258e486e9a 100644 (file)
--- 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
           "<tr>
            <td valign=\"top\">%d.</td>
+           <td><span class=\"uri\">%s</span></td>
+           </tr>
+           <tr>
+           <td />
            <td><ht:OBJECT uri=\"%s\" mode=\"%s\"/></td>
            </tr>%s"
-          !idx uri mode i)
+          !idx uri uri mode i)
       result ""
    in
    template query_kind
Unnamed repository; edit this file 'description' to name the repository.