From 7666f9dddfcaca5671dd25d3cd2095481968c7bf Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 4 Feb 2020 00:31:54 +0100 Subject: [PATCH] =?utf8?q?update=20in=20binaries=20for=20=CE=BB=CE=B4?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit roles: WIP ... --- .../contribs/lambdadelta/bin/roles/Makefile | 7 ++- .../contribs/lambdadelta/bin/roles/roles.css | 57 +++++++++++++++++++ .../lambdadelta/bin/roles/rolesEngine.ml | 4 ++ .../lambdadelta/bin/roles/rolesEngine.mli | 5 ++ .../lambdadelta/bin/roles/rolesUtils.ml | 20 +++++++ .../lambdadelta/bin/roles/rolesUtils.mli | 4 ++ .../lambdadelta/bin/roles/webEngine.ml | 25 ++++++++ 7 files changed, 120 insertions(+), 2 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/bin/roles/roles.css diff --git a/matita/matita/contribs/lambdadelta/bin/roles/Makefile b/matita/matita/contribs/lambdadelta/bin/roles/Makefile index 779952bac..8c34181a0 100644 --- 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 index 000000000..768c9afb2 --- /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 285807169..73cca4e66 100644 --- 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 4ccae9de0..fbaac551a 100644 --- 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 7c779fddf..ae8dc9fe0 100644 --- 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 252162e89..6fb3bab57 100644 --- 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 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 "
\n" c; + KP.printf "%s:\n" str; + KP.printf "%s\n" count; + KP.printf "
\n"; + KP.printf "
\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 "\n" c s str + in + let after_atoms () = + KP.printf "
%s
\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 () -- 2.39.2