From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 6 Jul 2014 14:41:50 +0000 (+0000)
Subject: - xhtbl: support for relative links added
X-Git-Tag: make_still_working~881
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c0d87c3cdf879f61aa53e91f43580e9815ae7190;p=helm.git

- xhtbl: support for relative links added
- web site: now the "forword" page is generated
---

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index c78a0d430..fb86723f5 100644
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -224,6 +224,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 05 Jul 2014 12:39:48 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 16:29:26 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile
index 3533cb02e..c88300d95 100644
--- a/helm/www/lambdadelta/Makefile
+++ b/helm/www/lambdadelta/Makefile
@@ -81,7 +81,7 @@ ifeq ($(MAKECMDGOALS), www)
 
    $(XSLS): $(TBLS) $(XHTBL)
 	@echo "  XHTBL *.tbl"
-	$(H)$(XHTBL) -O $(XSLTDIR) $(TBLS)
+	$(H)$(XHTBL) -b $(LDURL) -O $(XSLTDIR) $(TBLS)
 
    $(foreach LDW,$(LDWS),$(eval $(call HTML_TEMPLATE,$(LDW),$(notdir $(LDW:%.ldw.xml=%)))))
 endif
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 96f58a97b..3cb582ae7 100644
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -195,6 +195,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 05 Jul 2014 12:39:48 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 16:29:26 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index a8588e72b..071ad9091 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -1303,6 +1303,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 05 Jul 2014 12:39:48 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 16:29:26 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/bin/xhtbl/attr.ml b/helm/www/lambdadelta/bin/xhtbl/attr.ml
new file mode 100644
index 000000000..36b3d0003
--- /dev/null
+++ b/helm/www/lambdadelta/bin/xhtbl/attr.ml
@@ -0,0 +1,20 @@
+module L = List
+
+module T = Table
+
+(* true for a row specification *)
+type 'a atom = 'a * bool * int option * int option
+
+type 'a atoms = 'a atom list
+
+let get_attr concat null a y x =
+   let map y x (c, b, x1, x2) = match b, x1, x2 with
+      | _    , None, None       -> c
+      | false, None, Some c2    -> if x <= c2 then c else null
+      | false, Some c1, None    -> if x >= c1 then c else null
+      | false, Some c1, Some c2 -> if x >= c1 && x <= c2 then c else null
+      | true , None, Some r2    -> if y <= r2 then c else null
+      | true , Some r1, None    -> if y >= r1 then c else null
+      | true , Some r1, Some r2 -> if y >= r1 && y <= r2 then c else null
+   in
+   concat (L.map (map y x) a)
diff --git a/helm/www/lambdadelta/bin/xhtbl/css.ml b/helm/www/lambdadelta/bin/xhtbl/css.ml
deleted file mode 100644
index 82a41e91c..000000000
--- a/helm/www/lambdadelta/bin/xhtbl/css.ml
+++ /dev/null
@@ -1,20 +0,0 @@
-module L = List
-
-module T = Table
-
-(* true for a row specification *)
-type atom = T.css * bool * int option * int option
-
-type atoms = atom list
-
-let get_css a y x =
-   let map y x (c, b, x1, x2) = match b, x1, x2 with
-      | _    , None, None       -> c
-      | false, None, Some c2    -> if x <= c2 then c else []
-      | false, Some c1, None    -> if x >= c1 then c else []
-      | false, Some c1, Some c2 -> if x >= c1 && x <= c2 then c else []
-      | true , None, Some r2    -> if y <= r2 then c else []
-      | true , Some r1, None    -> if y >= r1 then c else []
-      | true , Some r1, Some r2 -> if y >= r1 && y <= r2 then c else []
-   in
-   L.concat (L.map (map y x) a)
diff --git a/helm/www/lambdadelta/bin/xhtbl/matrix.ml b/helm/www/lambdadelta/bin/xhtbl/matrix.ml
index 86d6f053a..62f6b194e 100644
--- a/helm/www/lambdadelta/bin/xhtbl/matrix.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/matrix.ml
@@ -1,10 +1,13 @@
 module A = Array
+module N = Filename
 
 module T = Table
 
 type cell = {
    ck: T.text list; (* contents *)
    cc: T.css;       (* css classes *)
+   cu: T.uri;       (* uri *)
+   cx: T.ext;       (* extension *)   
    cb: T.border;    (* border *)
 }
 
@@ -15,7 +18,7 @@ type matrix = {
 }
 
 let empty = {
-   ck = []; cc = []; cb = T.border false;
+   ck = []; cc = []; cu = ""; cx = ""; cb = T.border false;
 }
 
 let make ts = {
@@ -26,8 +29,12 @@ let make ts = {
 let set_key m y x kl = 
    m.m.(y).(x) <- {m.m.(y).(x) with ck = kl}
 
-let set_css m y x c = 
-   m.m.(y).(x) <- {m.m.(y).(x) with cc = c @ m.m.(y).(x).cc}
+let set_attrs m y x c u e = 
+   m.m.(y).(x) <- {m.m.(y).(x) with
+      cc = c @ m.m.(y).(x).cc;
+      cu = u ^ m.m.(y).(x).cu;
+      cx = m.m.(y).(x).cx ^ e;
+   }
 
 let set_west m y x b =
    let c = m.m.(y).(x) in
diff --git a/helm/www/lambdadelta/bin/xhtbl/options.ml b/helm/www/lambdadelta/bin/xhtbl/options.ml
index ce1c88867..21ebec1d9 100644
--- a/helm/www/lambdadelta/bin/xhtbl/options.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/options.ml
@@ -1,5 +1,7 @@
 let output_dir_default = ""
 
+let baseuri_default = ""
+
 let debug_lexer_default = false
 
 let debug_pass_default = false
@@ -8,6 +10,8 @@ let pass_default = false
 
 let output_dir = ref output_dir_default
 
+let baseuri = ref baseuri_default
+
 let debug_lexer = ref debug_lexer_default
 
 let d0 = ref debug_pass_default
@@ -28,6 +32,7 @@ let p2 = ref pass_default
 
 let clear () =
    output_dir := output_dir_default;
+   baseuri := baseuri_default;
    debug_lexer := debug_lexer_default;
    d0 := debug_pass_default; d1 := debug_pass_default; d2 := debug_pass_default; 
    e1 := debug_pass_default; e2 := debug_pass_default;
diff --git a/helm/www/lambdadelta/bin/xhtbl/pass1.ml b/helm/www/lambdadelta/bin/xhtbl/pass1.ml
index 1c53e7d6f..bedd9619f 100644
--- a/helm/www/lambdadelta/bin/xhtbl/pass1.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/pass1.ml
@@ -6,10 +6,12 @@ module F = Fold
 type status = {
    ts: T.size; (* current dimensions *)
    tc: T.css;  (* current class *)
+   tu: T.uri;  (* current uri *)
+   tx: T.ext;  (* current extension *)
 }
 
 let empty = {
-   ts = T.no_size; tc = [];
+   ts = T.no_size; tc = []; tu = ""; tx = ""
 }
 
 let init b ts =
@@ -38,8 +40,8 @@ let deinit ts = {ts with
 (****************************************************************************)
 
 let open_table st t =
-   t.T.tc <- t.T.tc @ st.tc;
-   {st with tc = t.T.tc}
+   t.T.tc <- t.T.tc @ st.tc; t.T.tu <- st.tu ^ t.T.tu; t.T.tx <- st.tx ^ t.T.tx; 
+   {st with tc = t.T.tc; tu = t.T.tu; tx = t.T.tx}
 
 let close_table st t =
    t.T.ts <- st.ts; st
diff --git a/helm/www/lambdadelta/bin/xhtbl/pass2.ml b/helm/www/lambdadelta/bin/xhtbl/pass2.ml
index 68cc7ba99..2e003ccb3 100644
--- a/helm/www/lambdadelta/bin/xhtbl/pass2.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/pass2.ml
@@ -50,11 +50,11 @@ let set_key st t = match t.T.te with
    | T.Key (T.Text sl) -> M.set_key st.tm t.T.ts.T.y t.T.ts.T.x sl  
    | _                 -> ()
 
-let set_css st t =
+let set_attrs st t =
    let rec aux y x =
       if y >= t.T.ts.T.rf then () else
       if x >= t.T.ts.T.cf then aux (succ y) 0 else begin
-	 M.set_css st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + x) t.T.tc;
+	 M.set_attrs st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + x) t.T.tc t.T.tu t.T.tx;
          aux y (succ x)
       end
    in
@@ -114,7 +114,7 @@ let open_table st t =
    print st t; st
 
 let close_table st t =
-   set_key st t; set_css st t; set_borders st t; st
+   set_key st t; set_attrs st t; set_borders st t; st
 
 let map_key st k = st
 
diff --git a/helm/www/lambdadelta/bin/xhtbl/pass3.ml b/helm/www/lambdadelta/bin/xhtbl/pass3.ml
index 4513828b5..337437709 100644
--- a/helm/www/lambdadelta/bin/xhtbl/pass3.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/pass3.ml
@@ -1,23 +1,31 @@
-module A = Array
+module L = List
+module S = String
+module V = Array
 
+module T = Table
 module M = Matrix
-module C = Css
+module A = Attr
 
 type status = {
    m: M.matrix;
-   a: C.atoms;
+   c: T.css A.atoms;
+   u: T.uri A.atoms;
+   x: T.ext A.atoms;
 }
 
-let initial a m = {
-   m = m; a = a;
+let initial c u x m = {
+   m = m; c = c; u = u; x = x
 }
 
 let process_cell st y x c =
-   M.set_css st.m y x (C.get_css st.a y x)
+   M.set_attrs st.m y x
+      (A.get_attr L.concat [] st.c y x)
+      (A.get_attr (S.concat "") "" st.u y x)
+      (A.get_attr (S.concat "") "" st.x y x)
 
 let process_row st y row =
-   A.iteri (process_cell st y) row
+   V.iteri (process_cell st y) row
 
-let process css matrix =
-   let st = initial css matrix in
-   A.iteri (process_row st) matrix.M.m
+let process css uri ext matrix =
+   let st = initial css uri ext matrix in
+   V.iteri (process_row st) matrix.M.m
diff --git a/helm/www/lambdadelta/bin/xhtbl/table.ml b/helm/www/lambdadelta/bin/xhtbl/table.ml
index 204df4c90..fe15c94db 100644
--- a/helm/www/lambdadelta/bin/xhtbl/table.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/table.ml
@@ -1,5 +1,11 @@
 type css = string list
 
+type uri = string
+
+type ext = string
+
+type absolute = bool
+
 type size = {
    y : int;         (* first row *)
    x : int;         (* first column *)
@@ -18,13 +24,15 @@ type border = {
 }
 
 type text = Plain of string
-          | Link of string * string
+          | Link of absolute * string * string
 
 type key = Text of text list
          | Glue of int option
 
 type table = {
    mutable tc: css;    (* css classes *)
+   mutable tu: uri;    (* uri *)
+   mutable tx: ext;    (* uri extension *)
    mutable ts: size;   (* dimension *)
            tb: border; (* border *)
            te: entry;  (* contents *)
@@ -46,12 +54,14 @@ let border b = {
    n = b; s = b; e = b; w = b;
 }
 
-let mk_key k tc = {
-   ts = no_size; tb = border false; te = Key k; tc = tc;
+let mk_key k tc tu tx = {
+   ts = no_size; tb = border false; te = Key k;
+   tc = tc; tu = tu; tx = tx;
    ti = id ();
 }
 
-let mk_line b tl tc = {
-   ts = no_size; tb = border b; te = Line (b, tl); tc = tc;
+let mk_line b tl tc tu tx = {
+   ts = no_size; tb = border b; te = Line (b, tl);
+   tc = tc; tu = tu; tx = tx;
    ti = id ();
 }
diff --git a/helm/www/lambdadelta/bin/xhtbl/textLexer.mll b/helm/www/lambdadelta/bin/xhtbl/textLexer.mll
index 7efa9035d..aa8f42fe4 100644
--- a/helm/www/lambdadelta/bin/xhtbl/textLexer.mll
+++ b/helm/www/lambdadelta/bin/xhtbl/textLexer.mll
@@ -26,13 +26,16 @@ rule token = parse
    | "("      { out "("; TP.OP                  }
    | ")"      { out ")"; TP.CP                  }   
    | "@"      { out ")"; TP.AT                  }    
-   | "space"  { out "name"; TP.SPACE            }
+   | "space"  { out "space"; TP.SPACE           }
    | "name"   { out "name"; TP.NAME             }   
    | "table"  { out "table"; TP.TABLE           }
    | "class"  { out "class"; TP.CSS             }
+   | "uri"    { out "uri"; TP.URI               }
+   | "ext"    { out "ext"; TP.EXT               }
    | eof      { TP.EOF                          }
 and str = parse
    | QT       { ""                              }
+   | "\\\\"   { "\\" ^ str lexbuf               }
    | "\\\""   { "\"" ^ str lexbuf               }
    | _ as c   { S.make 1 c ^ str lexbuf         }
 and block = parse
diff --git a/helm/www/lambdadelta/bin/xhtbl/textParser.mly b/helm/www/lambdadelta/bin/xhtbl/textParser.mly
index 3864bc53c..3dba122d0 100644
--- a/helm/www/lambdadelta/bin/xhtbl/textParser.mly
+++ b/helm/www/lambdadelta/bin/xhtbl/textParser.mly
@@ -7,18 +7,23 @@ module T = Table
 let split s =
    S.split (S.regexp "[ \r\n\t]+") s
 
-let mk_atom s rs =
-   let map c (b, (x1, x2)) = c, b, x1, x2 in 
-   L.map (map (split s)) rs
+let mk_css_atom s rs =
+   let cs = split s in
+   let map (b, (x1, x2)) = cs, b, x1, x2 in 
+   L.map map rs
+
+let mk_string_atom s rs =
+   let map (b, (x1, x2)) = s, b, x1, x2 in 
+   L.map map rs
 
 %}
 
 %token <int> NUM
 %token <string> TEXT 
-%token SPACE NAME TABLE CSS SR OC CC OB CB PS OP CP AT EOF
+%token SPACE NAME TABLE CSS URI EXT SR OC CC OB CB PS OP CP AT EOF
 
 %start script
-%type <(string * string) list * (string * Table.table * Css.atoms) list> script
+%type <(string * string) list * (string * Table.table * Table.css Attr.atoms * Table.uri Attr.atoms * Table.ext Attr.atoms) list> script
 
 %%
 
@@ -32,8 +37,11 @@ spaces:
 ;
 
 text:
-   | TEXT               { T.Plain $1 }
-   | AT OP TEXT TEXT CP { T.Link ($3, $4) }
+   | TEXT                  { T.Plain $1             }
+   | AT OP TEXT TEXT CP    { T.Link (true, $3, $4)  }
+   | AT AT OP TEXT TEXT CP { T.Link (false, $4, $5) }
+   | AT TEXT               { T.Link (true, $2, $2)  }
+   | AT AT TEXT            { T.Link (false, $3, $3) }   
 ;
 
 texts:
@@ -52,10 +60,20 @@ css:
    | CSS TEXT { split $2 }
 ;
 
+uri:
+   |          { "" }
+   | URI TEXT { $2 }
+;
+
+ext:
+   |          { "" }
+   | EXT TEXT { $2 }
+;
+
 table:
-   | css key          { T.mk_key        $2 $1 }
-   | css OC tables CC { T.mk_line false $3 $1 }
-   | css OB tables CB { T.mk_line true  $3 $1 }
+   | css uri ext key          { T.mk_key        $4 $1 $2 $3 }
+   | css uri ext OC tables CC { T.mk_line false $5 $1 $2 $3 }
+   | css uri ext OB tables CB { T.mk_line true  $5 $1 $2 $3 }
 ;
 
 tables:
@@ -87,17 +105,35 @@ ranges:
    | range ranges { $1 :: $2 }
 ;
 
-atom:
-   | CSS TEXT ranges { mk_atom $2 $3 }
+catom:
+   | CSS TEXT ranges { mk_css_atom $2 $3 }
+;
+
+catoms:
+   |              { []      }
+   | catom catoms { $1 @ $2 }
+;
+
+uatom:
+   | URI TEXT ranges { mk_string_atom $2 $3 }
+;
+
+uatoms:
+   |              { []      }
+   | uatom uatoms { $1 @ $2 }
+;
+
+xatom:
+   | EXT TEXT ranges { mk_string_atom $2 $3 }
 ;
 
-atoms:
-   |            { []      }
-   | atom atoms { $1 @ $2 }
+xatoms:
+   |              { []      }
+   | xatom xatoms { $1 @ $2 }
 ;
 
 directive:
-   | name TABLE table atoms { $1, $3, $4 }
+   | name TABLE table catoms uatoms xatoms { $1, $3, $4, $5, $6 }
 ;
 
 directives:
diff --git a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml
index fec699bcb..ece6949d9 100644
--- a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml
@@ -41,9 +41,13 @@ let border tb =
 let css tc =
    P.sprintf "\"%s\"" (S.concat " " tc)
 
+let uri tu tx =
+   P.sprintf "@\"%s\" \"%s\"" tu tx
+
 let text = function
-   | T.Plain s       -> P.sprintf "\"%s\"" s
-   | T.Link (uri, s) -> P.sprintf "@(\"%s\" \"%s\")" uri s
+   | T.Plain s              -> P.sprintf "\"%s\"" s
+   | T.Link (true, uri, s)  -> P.sprintf "@(\"%s\" \"%s\")" uri s
+   | T.Link (false, uri, s) -> P.sprintf "@@(\"%s\" \"%s\")" uri s
 
 let key = function
    | T.Text sl       -> S.concat " + " (L.map text sl)
@@ -58,8 +62,8 @@ let entry = function
 
 let open_table st t =
    let str = 
-      P.sprintf "%s[{#%u: %s; %s; %s}\n"    
-         (indent st) t.T.ti (size t.T.ts) (border t.T.tb) (css t.T.tc)
+      P.sprintf "%s[{#%u: %s; %s; %s; %s}\n"    
+         (indent st) t.T.ti (size t.T.ts) (border t.T.tb) (css t.T.tc) (uri t.T.tu t.T.tx)
    in
    st.out str; add st
 
diff --git a/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml b/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml
index f379185fa..6c5f8b01f 100644
--- a/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml
@@ -16,6 +16,7 @@ let help    = "Usage: xhtbl [ -LX | -O <dir> | -d0 | -d1 | -d2 | -e1 | -e2 | -p0
 let help_L  = " Output lexer tokens"
 let help_O  = "<dir>  Set this output directory"
 let help_X  = " Clear all options"
+let help_b  = "<uri>  Set this base uri for relative links"
 let help_d0 = " Output table contents after phase zero (parsing)"
 let help_d1 = " Output table contents after phase one (sizing)"
 let help_d2 = " Output table contents after phase two (filling)"
@@ -29,9 +30,7 @@ let hook = "xhtbl"
 
 let includes, tables = ref [], ref []
 
-let set_output_dir s = O.output_dir := s
-
-let process_directive och bname (name, table, css) =
+let process_directive och bname (name, table, css, uri, ext) =
    tables := name :: !tables;
    if !O.d0 then TU.debug table;
    if not !O.p0 then begin
@@ -41,7 +40,7 @@ let process_directive och bname (name, table, css) =
          let matrix = M.make size in
          let _ = P2.process table matrix in
          if !O.d2 then TU.debug table;
-         if not !O.p2 then P3.process css matrix;
+         if not !O.p2 then P3.process css uri ext matrix;
 	 let name = if name = "" then bname else name in
          XU.output och name matrix
       end
@@ -61,8 +60,9 @@ let process_file fname =
 let main () =
    A.parse [
       "-L", A.Set O.debug_lexer, help_L;
-      "-O", A.String set_output_dir, help_O; 
+      "-O", A.String ((:=) O.output_dir), help_O; 
       "-X", A.Unit O.clear, help_X;
+      "-b", A.String ((:=) O.baseuri), help_b;
       "-d0", A.Set O.d0, help_d0;  
       "-d1", A.Set O.d1, help_d1;  
       "-d2", A.Set O.d2, help_d2;  
diff --git a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml
index f413aa0ef..603c7f1be 100644
--- a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml
@@ -22,12 +22,15 @@ let border cell =
    if cell.M.cb.T.w then str.[3] <- 's';
    str :: cell.M.cc
 
-let text = function
-   | T.Plain s       -> s
-   | T.Link (uri, s) -> P.sprintf "<a href=\"%s\">%s</a>" uri s
+let text baseuri ext = function
+   | T.Plain s              -> s
+   | T.Link (true, uri, s)  -> P.sprintf "<a href=\"%s\">%s</a>" uri s
+   | T.Link (false, uri, s) -> 
+      let uri = !O.baseuri ^ baseuri ^ uri ^ ext in
+      P.sprintf "<a href=\"%s\">%s</a>" uri s
 
 let key cell =
-   if cell.M.ck = [] then "<br/>" else S.concat " " (L.map text cell.M.ck)
+   if cell.M.ck = [] then "<br/>" else S.concat " " (L.map (text cell.M.cu cell.M.cx) cell.M.ck)
 
 let ind i = S.make (2 * i) ' '
 
diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css
index ed3a266f5..150aaf781 100644
--- a/helm/www/lambdadelta/css/ld_web.css
+++ b/helm/www/lambdadelta/css/ld_web.css
@@ -8,14 +8,20 @@ body {
    margin: 2.5%;
 }
 
-a:link, a:visited {
+a:link, a:visited, a:hover, a:active, a:focus {
    text-decoration: underline;
    color: rgb(0, 0, 0);
 }
 
-a:active, a:hover, a:focus {
+a:hover {
    background: rgb(192, 192, 192);
-   color: rgb(0, 0, 0);
+}
+
+/* on newer browsers, disable style modifications for named anchors */
+a[name]:hover {
+   text-decoration: inherit;
+   color: inherit;
+   background: inherit;
 }
 
 /* blocks *******************************************************************/
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index c5c5b833d..e6f303995 100644
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -237,6 +237,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 05 Jul 2014 12:39:48 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 16:29:26 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 07e98c6a9..ce113aff0 100644
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -1,145 +1,146 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
-<html dir="ltr" lang="en-us"><head>
-
-
-
-  <meta content="text/html; charset=UTF-8" http-equiv="content-type"><title>λδ home page</title>
-  
-  <meta content="Ferruccio Guidi" name="author">
-  <meta content="The formal system λδ" name="description">
-  <link rel="shortcut icon" href="images/crux_16.ico"></head><body>
-<div style="text-align: center;">
-<br>
-<a href="http://lambdadelta.info/"><img alt="[Crux Logo]" title="The Crux" src="images/crux_32.png" style="border: 0px solid ; width: 32px; height: 32px;"></a>
-<h1>The Formal System λδ (\lambda\delta)<br>
-</h1>
-<h2>Towards the unification of terms, types, environments and contexts</h2>
-<img style="width: 95%; height: 4px;" alt="[Separator]" title="Separator" src="images/rainbow.png"><br>
-<table style="text-align: left; width: 95%; margin-left: auto; margin-right: auto;" border="0" cellpadding="2" cellspacing="20">
-  <tbody>
-    <tr>
-      <td style="vertical-align: top;">
-      <ul>
-        <li>Foreword</li>
-      </ul>
-      <ul>
-        <li><a href="news.html">News</a></li>
-      </ul>
-      <ul>
-        <li><a href="documentation.html">Papers</a></li>
-      </ul>
-      <ul>
-        <li><a href="implementation.html">Resources</a><br>
-        </li>
-      </ul>
-      </td>
-      <td style="vertical-align: top; text-align: left;">
-      <h3 style="text-align: right;">Foreword <img style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" src="images/b9.png"></h3>
-The formal system λδ
-(\lambda\delta) is a typed lambda calculus that pursues the static and
-dynamic unification of terms, types, environments and contexts while
-enjoying a well-conceived theory, which includes the commonly
-desired properties.<br>
-      <br>
-λδ takes some features from the calculi of the Automath family and
-some from the pure type systems, but it differs from both in that it
-does not include the Π construction while it provides for an
-abbreviation mechanism at the level of terms.<br>
-      <br>
-λδ features explicit type annotations, which are borrowed from
-realistic type checker implementations and with which type checking is
-reduced to type inference.<br>
-      <br>
-The reduction steps of λδ include β-contraction, δ-expansion,
-ζ-contraction and θ-swap. On the other hand,
-η-contraction is not included.<br>
-      <br>
-The theory of λδ includes important properties such as the
-confluence of reduction, the correctness of types, the
-uniqueness of types up to conversion, the subject reduction of the type
-assignment, the strong normalization of the typed terms. The
-decidability of type inference and of type checking come as corollaries.<br>
-      <br>
-λδ features uniformly dependent types and a predicative abstraction
-mechanism, so the calculus can serve as a formal specification language
-for the type theories that need a predicative foundation. λδ is
-expected to have the expressive power of λ→.<br>
-      <br>
-λδ comes in several versions listed in the following table, which
-includes the major milestones:<br>
-      <br>
-      <table style="text-align: left; width: 100%;" border="1" cellpadding="2" cellspacing="0">
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
+  <head>
+    <meta http-equiv="Content-Language" content="en-us" />
+    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
+    <meta http-equiv="Content-Style-Type" content="text/css" />
+    <meta name="author" content="Ferruccio Guidi" />
+    <meta name="description" content="\lambda\delta home page" />
+    <title>\lambda\delta home page</title>
+    <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
+    <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
+    <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
+    <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
+  </head>
+  <body lang="en-US">
+    <div class="spacer">
+      <a href="http://lambdadelta.info/">
+        <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
+      </a>
+    </div>
+    <div class="head1">The Formal System λδ (\lambda\delta)</div>
+    <div class="spacer">
+      <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
+    </div>
+   <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+      <br />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
         <tbody>
           <tr>
-            <td style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Version<br>
+            <td class="snss component sky">
+              <a href="http://lambdadelta.info/index.html">foreword</a>
             </td>
-            <td style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Name<br>
+            <td class="snss component magenta">
+              <a href="http://lambdadelta.info/news.html">news</a>
             </td>
-            <td style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Started<br>
+            <td class="snss component orange">
+              <a href="http://lambdadelta.info/documentation.html">documentation</a>
             </td>
-            <td style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Released<br>
-            </td>
-            <td style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Dismissed<br>
+            <td class="ssss component green">
+              <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
           </tr>
+        </tbody>
+      </table>
+    </div>
+
+   <a xmlns:ld="http://lambdadelta.info/" name="foreword" />
+    <div xmlns:ld="http://lambdadelta.info/" class="head2dx">Foreword <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
+    </div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support
+      the foundations of Mathematics that require an underlying specification language
+      (for example the <a href="http://www.math.unipd.it/~maietti/">Minimal Type Theory</a>
+       and its predecessors).
+   </div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      λδ is developed in the context of the
+      <a href="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</a>
+      as a machine-checked digital specification
+      that is not the formal counterpart of some previously published informal material.
+   </div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      λδ comes in several versions listed in the following table,
+      which includes the major milestones:
+   </div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
+        <tbody>
           <tr>
-            <td style="vertical-align: top; background-color: rgb(255, 223, 191);">2<br>
-            </td>
-            <td style="vertical-align: top; background-color: rgb(255, 223, 191);">basic_2<br>
-            </td>
-            <td style="vertical-align: top; background-color: rgb(255, 223, 191);">April
-2011<br>
-            </td>
-            <td style="vertical-align: top; background-color: rgb(255, 223, 191);">planned
-in
-2014<br>
-            </td>
-            <td style="vertical-align: top; background-color: rgb(255, 223, 191);">not
-planned yet<br>
-            </td>
+            <td class="snns component gray">version</td>
+            <td class="snnn component gray">name</td>
+            <td class="snnn component gray">developed with</td>
+            <td class="snnn component gray">started</td>
+            <td class="snnn component gray">announced</td>
+            <td class="snnn component gray">released</td>
+            <td class="ssnn component gray">dismissed</td>
           </tr>
           <tr>
-            <td style="vertical-align: top; background-color: rgb(255, 191, 191);">1<br>
-            </td>
-            <td style="vertical-align: top; background-color: rgb(255, 191, 191);">basic_1<br>
-            </td>
-            <td style="vertical-align: top; background-color: rgb(255, 191, 191);">May
-2004<br>
+            <td class="snns orange">2</td>
+            <td class="snnn orange">basic_2</td>
+            <td class="snnn orange">
+              <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>
             </td>
-            <td style="vertical-align: top; background-color: rgb(255, 191, 191);">November
-2006<br>
-            </td>
-            <td style="vertical-align: top; background-color: rgb(255, 191, 191);">May
-2008<br>
+            <td class="snnn orange">April 2011</td>
+            <td class="snnn orange">July 2014</td>
+            <td class="snnn orange">Planned in 2014</td>
+            <td class="ssnn orange">Not planned yet</td>
+          </tr>
+          <tr>
+            <td class="snss red">1</td>
+            <td class="snsn red">basic_1</td>
+            <td class="snsn red">
+              <a href="http://coq.inria.fr/">Coq 7.3.1</a>
             </td>
+            <td class="snsn red">May 2004</td>
+            <td class="snsn red">January 2006</td>
+            <td class="snsn red">November 2006</td>
+            <td class="sssn red">May 2008</td>
           </tr>
         </tbody>
       </table>
-      <br>
-      <h3 style="text-align: right;">Notice
-for
-the
-Internet
-Explorer
-user <img style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" src="images/b3.png"></h3>
-To view this site
-correctly, please select a font with <a href="http://www.unicode.org/">Unicode</a>
-support.
-For example <span style="font-weight: bold;">Lucida Sans Unicode</span>
-(it should be already installed on your system).
-To change the current font follow: <span style="font-weight: bold;">"Tools"
-menu
-→ "Internet
-Options" entry → "General" tab → "Fonts" button.</span><br>
-      </td>
-    </tr>
-  </tbody>
-</table>
-<br>
-<a href="http://validator.w3.org/check?uri=referer"><img alt="[Valid HTML 4.01 Transitional]" title="Valid HTML 4.01 Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"></a> <a href="http://www.anybrowser.org/campaign/"><img alt="[Use Any Browser Here]" title="Use Any Browser Here" src="images/globe_trans.png" style="border: 0px solid ; width: 147px; height: 42px;"></a> <img style="width: 88px; height: 31px;" alt="[PNG Used Here]" title="PNG Used Here" src="images/PNGnow2.png"><br>
-<br>
-Last update 2014-02-24 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
-Guidi</a><br>
-</div>
+    </div>
+
+   <a xmlns:ld="http://lambdadelta.info/" name="notice" />
+    <div xmlns:ld="http://lambdadelta.info/" class="head2dx">Notice for the Internet Explorer user <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b3.png" />
+    </div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      To view this site correctly, please select a font
+      with <a href="http://www.unicode.org/">Unicode</a> support.
+      For example "Lucida Sans Unicode" (it should be already installed on your system).
+      To change the current font follow:
+      "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
+   </div>
 
-</body></html>
+   <div class="spacer">
+      <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+      <br />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+      <a href="http://validator.w3.org/check?uri=referer">
+        <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
+      </a>
+      <a href="http://jigsaw.w3.org/css-validator/check/referer">
+        <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
+      </a>
+      <a href="http://www.w3.org/XML/">
+        <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
+      </a>
+      <a href="http://www.w3.org/Graphics/PNG/">
+        <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
+      </a>
+      <a href="http://www.anybrowser.org/campaign/">
+        <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
+      </a>
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+      <br />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 16:37:09 +0200</div>
+</body>
+</html>
diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml
new file mode 100644
index 000000000..14be7fa88
--- /dev/null
+++ b/helm/www/lambdadelta/web/home/index.ldw.xml
@@ -0,0 +1,39 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+      description = "\lambda\delta home page"
+      title = "\lambda\delta home page"
+      head = "The Formal System λδ (\lambda\delta)"
+>
+   <sitemap name="sitemap"/>
+
+   <section9 name="foreword">Foreword</section9>
+   <body>
+      The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support
+      the foundations of Mathematics that require an underlying specification language
+      (for example the <link to="http://www.math.unipd.it/~maietti/">Minimal Type Theory</link>
+       and its predecessors).
+   </body>
+   <body>
+      λδ is developed in the context of the
+      <link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</link>
+      as a machine-checked digital specification
+      that is not the formal counterpart of some previously published informal material.
+   </body>
+   <body>
+      λδ comes in several versions listed in the following table,
+      which includes the major milestones:
+   </body>
+   <table name="versions"/>
+
+   <section3 name="notice">Notice for the Internet Explorer user</section3>
+   <body>
+      To view this site correctly, please select a font
+      with <link to="http://www.unicode.org/">Unicode</link> support.
+      For example "Lucida Sans Unicode" (it should be already installed on your system).
+      To change the current font follow:
+      "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
+   </body>
+
+   <footer/>
+</page>
diff --git a/helm/www/lambdadelta/web/home/index2.ldw.xml b/helm/www/lambdadelta/web/home/index2.ldw.xml
deleted file mode 100644
index 14be7fa88..000000000
--- a/helm/www/lambdadelta/web/home/index2.ldw.xml
+++ /dev/null
@@ -1,39 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-
-<page xmlns="http://lambdadelta.info/"
-      description = "\lambda\delta home page"
-      title = "\lambda\delta home page"
-      head = "The Formal System λδ (\lambda\delta)"
->
-   <sitemap name="sitemap"/>
-
-   <section9 name="foreword">Foreword</section9>
-   <body>
-      The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support
-      the foundations of Mathematics that require an underlying specification language
-      (for example the <link to="http://www.math.unipd.it/~maietti/">Minimal Type Theory</link>
-       and its predecessors).
-   </body>
-   <body>
-      λδ is developed in the context of the
-      <link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics</link>
-      as a machine-checked digital specification
-      that is not the formal counterpart of some previously published informal material.
-   </body>
-   <body>
-      λδ comes in several versions listed in the following table,
-      which includes the major milestones:
-   </body>
-   <table name="versions"/>
-
-   <section3 name="notice">Notice for the Internet Explorer user</section3>
-   <body>
-      To view this site correctly, please select a font
-      with <link to="http://www.unicode.org/">Unicode</link> support.
-      For example "Lucida Sans Unicode" (it should be already installed on your system).
-      To change the current font follow:
-      "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
-   </body>
-
-   <footer/>
-</page>
diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl
index 78a5a2da0..7e2969bc9 100644
--- a/helm/www/lambdadelta/web/home/sitemap.tbl
+++ b/helm/www/lambdadelta/web/home/sitemap.tbl
@@ -2,17 +2,19 @@ name "sitemap"
 
 table [
    class "sky" {
-      [ "foreword" * ]
+      [ @@("index" "foreword") * ]
    }
    class "magenta" {
-      [ "news" * ]
+      [ @@"news" * ]
    }
    class "orange" {
-      [ "bibliography" * ]
+      [ @@"documentation" * ]
    }
    class "green" {
-      [ "resources" * ]
+      [ @@"implementation" * ]
    }
 ]
 
 class "component" [ 0 ]
+
+ext ".html" [ 0 ]