update in binaries for λδ

roles: WIP ...

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/Makefile b/matita/matita/contribs/lambdadelta/bin/roles/Makefile
index 779952bacd13edc61af1bff74be3da04dd7b96c3..8c34181a09abba3db6d9b71d25285f425b0f5e7f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/Makefile
+++ b/matita/matita/contribs/lambdadelta/bin/roles/Makefile
@@ -5,6 +5,9 @@ REQUIRES =
 include ../Makefile.common
 
 test:
-#      @$(MAKE) --no-print-directory -C ../../ www
+       @./roles.native -C ../.. -r -W > roles.html
 
-.PHONY: test
+up-css:
+       @scp roles.css lahar.helm.cs.unibo.it:/projects/helm/public_html/lambdadelta/css/
+
+.PHONY: test up-css

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/roles.css b/matita/matita/contribs/lambdadelta/bin/roles/roles.css
new file mode 100644 (file)
index 0000000..768c9af
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/roles/roles.css
@@ -0,0 +1,57 @@
+@charset "UTF-8";
+
+/* anchors ******************************************************************/
+
+a:link {
+  text-decoration: initial;
+  color: inherit;
+}
+
+/* visited link */
+a:visited {
+  text-decoration: initial;
+  color: inherit;
+}
+
+/* mouse over link */
+a:hover {
+  text-decoration: underline;
+  color: inherit;
+}
+
+/* selected link */
+a:active {
+  text-decoration: underline;
+  color: inherit;
+}
+
+/* layouts ******************************************************************/
+
+.atoms-head {
+}
+
+.count {
+}
+
+.atoms {
+  overflow-x: auto;
+  border-bottom: 0.5em solid white;
+}
+
+.atom {
+  padding: 0.25em 0.5em;
+}
+
+.selected {
+  border: 1pt dotted;
+}
+
+/* colors *******************************************************************/
+
+.object {
+  color: skyblue;
+}
+
+.name {
+  color: darkseagreen;
+}

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
index 285807169f05696a37ab673f422c5cdc0f985358..73cca4e6618da4ab5499a2cccbbedac16a3ae12b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
@@ -102,3 +102,7 @@ let write_status () =
 
 let print_status () =
   EO.out_status stdout st
+
+let visit_status before_t each_t after_t before_w each_w after_w =
+  EU.list_visit before_t each_t after_t EU.string_of_obj [1] st.ET.t;
+  EU.list_visit before_w each_w after_w EU.string_of_name [2] st.ET.w

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli
index 4ccae9de0391df84fd645683590ddb8a2c6fb088..fbaac551ac19fffddac0abce6b65611a1c8f83eb 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli
@@ -26,3 +26,8 @@ val read_status: unit -> unit
 val write_status: unit -> unit
 
 val print_status: unit -> unit
+
+val visit_status:
+  (string -> string -> unit) -> (string -> bool -> string -> unit) -> (unit -> unit) ->
+  (string -> string -> unit) -> (string -> bool -> string -> unit) -> (unit -> unit) ->
+  unit

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
index 7c779fddfebdcf6aadcad2d331c158eba49e0acc..ae8dc9fe0beea34def9771f3e81085da6ce0d14e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
@@ -74,6 +74,10 @@ let rec list_exists compare = function
     if b <= 0 then b = 0 else
     list_exists compare tl
 
+let rec list_count s c = function
+  | []         -> s, c
+  | (b, _)::tl -> list_count (s + if b then 1 else 0) (succ c) tl
+
 let string_of_version v =
   String.concat "." (List.map string_of_int v)
 
@@ -163,8 +167,24 @@ let new_status = {
   ET.r = []; ET.s = []; ET.t = []; ET.w = [];
 }
 
+let string_of_pointer = string_of_version 
+
 let pointer_of_string = version_of_string
 
+let list_visit before each after string_of p l =
+  let ptr p = string_of_pointer (List.rev p) in
+  let rec aux i = function
+    | []         -> ()
+    | (b, x)::tl ->
+      each (ptr (i::p)) b (string_of x);
+      aux (succ i) tl
+  in
+  let s, c = list_count 0 0 l in
+  let count = Printf.sprintf "%u/%u" s c in
+  before (ptr p) count;
+  aux 0 l;
+  after ()
+
 let string_of_error = function
   | ET.EWrongExt x   ->
     Printf.sprintf "unknown input file type %S" x

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli
index 252162e892989ef7c9b17c9d95bf59b37d22c0d4..6fb3bab57ea8653b289974d1ea8c09d770c81f81 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli
@@ -21,6 +21,10 @@ val list_split: (bool * 'b) list -> (bool * 'b) list * (bool * 'b) list
 
 val list_select: 'b option -> (bool * 'b) list -> 'b option
 
+val list_visit:
+  (string -> string -> unit) -> (string -> bool -> string -> unit) -> (unit -> unit) ->
+  ('a -> string) -> RolesTypes.pointer -> (bool * 'a) list -> unit
+
 val string_of_version: RolesTypes.version -> string
 
 val version_of_string: string -> RolesTypes.version

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml
index 7fc9429605ca57c97f75b3a2fe5c9547ca7688a5..5dcc26e3618467a3ab543e7fa29ed2770f81be70 100644 (file)
--- 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 ()