X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Froles%2FwebEngine.ml;h=5dcc26e3618467a3ab543e7fa29ed2770f81be70;hp=7fc9429605ca57c97f75b3a2fe5c9547ca7688a5;hb=7666f9dddfcaca5671dd25d3cd2095481968c7bf;hpb=2c9f4fddc259b09b6e71b18eef78f0bed38eeb14

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml
index 7fc942960..5dcc26e36 100644
--- a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml
@@ -53,6 +53,31 @@ let open_out () =
 let close_out () =
   close_out_html ()
 
+let status_out () =
+  let before_atoms a p count =
+    let c, str =
+      if a then "object", "objects"
+      else "name", "names"
+    in
+    KP.printf "<div class=\"atoms-head %s\">\n" c;
+    KP.printf "<a href=\"\">%s:</a>\n" str;
+    KP.printf "<span class=\"count\">%s</span>\n" count;
+    KP.printf "</div>\n";
+    KP.printf "<div class=\"atoms\"><table><tr>\n"
+  in
+  let each_atom a p b str =
+    let c = if a then "object" else "name" in
+    let s = if b then " selected" else "" in
+    KP.printf "<td class=\"atom %s%s\"><a href=\"\">%s</a></td>\n" c s str
+  in
+  let after_atoms () =
+    KP.printf "</tr></table></div>\n"
+  in
+  EE.visit_status
+    (before_atoms true) (each_atom true) after_atoms
+    (before_atoms false) (each_atom false) after_atoms
+
 let init () =
   open_out ();
+  status_out ();
   close_out ()