- new pretty printing of interpretations

[helm.git] / helm / searchEngine / mooglePp.ml

diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml
index 7731eb28802998de47f3e10ae6ce0c9133664eec..92b55668e5cbe9aa1f5e69194df01c8887d7b37b 100644 (file)
--- a/helm/searchEngine/mooglePp.ml
+++ b/helm/searchEngine/mooglePp.ml
@@ -59,18 +59,26 @@ let theory_of_result page result =
     ("no results found", "")
 
 let html_of_interpretations interps =
-  let radio_button n = 
-    sprintf "<input type=\"radio\" name=\"param.interp\" value=\"%d\" />" n
+  let choice_of_interp interp =
+    sprintf "<table>\n%s\n</table>"
+      (String.concat "\n"
+        (List.map
+           (fun (k, v) ->
+              sprintf "<tr><td><em>%s</em></td><td>%s</td></tr>" k v)
+           interp))
   in
-  let text interp =
-    String.concat "<br />" 
-      (List.map
-         (fun (id, value) -> sprintf "<span>%s = %s</span>" id value)
-         interp)
-  in
-  let rec aux n = function
-    | [] -> []
-    | interp::tl -> ((radio_button n)^(text interp))::(aux (n+1) tl)
-  in
-  String.concat "<br />" (aux 0 interps)
+  let interp_no = ref ~-1 in
+    sprintf "<table class=\"interp\">\n%s\n</table>"
+      (String.concat "\n"
+        (List.map
+           (fun interp ->
+              sprintf "
+                  <tr class=\"interp\">
+                  <td><input type=\"radio\" name=\"param.interp\" value=\"%d\" /></td>
+                  <td>
+                  %s
+                  </td></tr>"
+                (incr interp_no; !interp_no)
+                (choice_of_interp interp))
+           interps))