From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 13 Jul 2014 21:35:30 +0000 (+0000)
Subject: - xhtbl : support for named anchors (id's) and other improvements
X-Git-Tag: make_still_working~874
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3167db4903eea2eddc60a91cfd922be3672ce077;p=helm.git

- xhtbl : support for named anchors (id's) and other improvements
- ld_web: additions for the "documentation" page
---

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index d21660ea7..338b38399 100644
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -223,6 +223,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 15:47:14 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 23:25:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 40e52f117..eb58a004c 100644
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -191,6 +191,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 15:47:14 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 23:25:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index b858c6cc3..d3356642f 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -1300,6 +1300,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 15:47:14 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 23:25:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/bin/xhtbl/matrix.ml b/helm/www/lambdadelta/bin/xhtbl/matrix.ml
index 62f6b194e..1c65c5004 100644
--- a/helm/www/lambdadelta/bin/xhtbl/matrix.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/matrix.ml
@@ -7,7 +7,8 @@ type cell = {
    ck: T.text list; (* contents *)
    cc: T.css;       (* css classes *)
    cu: T.uri;       (* uri *)
-   cx: T.ext;       (* extension *)   
+   cx: T.ext;       (* extension *)
+   cn: T.anchor;    (* named anchor *)   
    cb: T.border;    (* border *)
 }
 
@@ -17,8 +18,10 @@ type matrix = {
    m: cell array array; (* matrix *)
 }
 
+let strand a b = if a = "" then b else a
+
 let empty = {
-   ck = []; cc = []; cu = ""; cx = ""; cb = T.border false;
+   ck = []; cc = []; cu = ""; cx = ""; cn = ""; cb = T.border false;
 }
 
 let make ts = {
@@ -29,11 +32,12 @@ let make ts = {
 let set_key m y x kl = 
    m.m.(y).(x) <- {m.m.(y).(x) with ck = kl}
 
-let set_attrs m y x c u e = 
+let set_attrs m y x c u e n = 
    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;
+      cn = strand m.m.(y).(x).cn n;
    }
 
 let set_west m y x b =
diff --git a/helm/www/lambdadelta/bin/xhtbl/pass2.ml b/helm/www/lambdadelta/bin/xhtbl/pass2.ml
index 2e003ccb3..549d7654e 100644
--- a/helm/www/lambdadelta/bin/xhtbl/pass2.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/pass2.ml
@@ -54,7 +54,7 @@ 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_attrs st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + x) t.T.tc t.T.tu t.T.tx;
+	 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 t.T.tn;
          aux y (succ x)
       end
    in
diff --git a/helm/www/lambdadelta/bin/xhtbl/pass3.ml b/helm/www/lambdadelta/bin/xhtbl/pass3.ml
index 337437709..d2455a30a 100644
--- a/helm/www/lambdadelta/bin/xhtbl/pass3.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/pass3.ml
@@ -22,6 +22,7 @@ let process_cell st y x c =
       (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 =
    V.iteri (process_cell st y) row
diff --git a/helm/www/lambdadelta/bin/xhtbl/table.ml b/helm/www/lambdadelta/bin/xhtbl/table.ml
index fe15c94db..d3ee13bfa 100644
--- a/helm/www/lambdadelta/bin/xhtbl/table.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/table.ml
@@ -4,6 +4,8 @@ type uri = string
 
 type ext = string
 
+type anchor = string
+
 type absolute = bool
 
 type size = {
@@ -30,6 +32,7 @@ type key = Text of text list
          | Glue of int option
 
 type table = {
+           tn: anchor; (* named anchor *)
    mutable tc: css;    (* css classes *)
    mutable tu: uri;    (* uri *)
    mutable tx: ext;    (* uri extension *)
@@ -54,14 +57,14 @@ let border b = {
    n = b; s = b; e = b; w = b;
 }
 
-let mk_key k tc tu tx = {
+let mk_key k tc tu tx tn = {
    ts = no_size; tb = border false; te = Key k;
-   tc = tc; tu = tu; tx = tx;
+   tc = tc; tu = tu; tx = tx; tn = tn;
    ti = id ();
 }
 
-let mk_line b tl tc tu tx = {
+let mk_line b tl tc tu tx tn = {
    ts = no_size; tb = border b; te = Line (b, tl);
-   tc = tc; tu = tu; tx = tx;
+   tc = tc; tu = tu; tx = tx; tn = tn;
    ti = id ();
 }
diff --git a/helm/www/lambdadelta/bin/xhtbl/textParser.mly b/helm/www/lambdadelta/bin/xhtbl/textParser.mly
index 587395988..9072c2b23 100644
--- a/helm/www/lambdadelta/bin/xhtbl/textParser.mly
+++ b/helm/www/lambdadelta/bin/xhtbl/textParser.mly
@@ -72,9 +72,9 @@ ext:
 ;
 
 table:
-   | 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 }
+   | css uri ext name key     { T.mk_key        $5 $1 $2 $3 $4 }
+   | 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:
diff --git a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml
index 339a9aeec..cf7724cdd 100644
--- a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml
@@ -44,6 +44,10 @@ let css tc =
 let uri tu tx =
    P.sprintf "@\"%s\" \"%s\"" tu tx
 
+let name tn =
+   P.sprintf "$\"%s\"" tn
+
+
 let text = function
    | T.Plain s              -> P.sprintf "\"%s\"" s
    | T.Link (true, uri, s)  -> P.sprintf "@(\"%s\" \"%s\")" uri s
@@ -62,8 +66,8 @@ let entry = function
 
 let open_table st t =
    let str = 
-      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)
+      P.sprintf "%s[{#%u: %s; %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) (name t.T.tn)
    in
    st.out str; add st
 
diff --git a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml
index e46682c3f..0ff801e93 100644
--- a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml
@@ -14,6 +14,13 @@ let myself = F.basename (Sys.argv.(0))
 
 let msg = P.sprintf "This file was generated by %s, do not edit" myself
 
+let compose uri ext =
+   try
+      let i = S.index uri '#' in
+      let uri, fragment = S.sub uri 0 i, S.sub uri i (S.length uri - i) in
+      uri ^ ext ^ fragment
+   with Not_found -> uri ^ ext
+
 let border cell =
    let str = S.make 4 'n' in
    if cell.M.cb.T.n then str.[0] <- 's';   
@@ -26,9 +33,12 @@ 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
+      let uri = !O.baseuri ^ baseuri ^ compose uri ext in
       P.sprintf "<a href=\"%s\">%s</a>" uri s
 
+let name cell =
+   if cell.M.cn = "" then "" else P.sprintf " id=\"%s\"" cell.M.cn
+
 let key cell =
    if cell.M.ck = [] then "<br/>" else S.concat "" (L.map (text cell.M.cu cell.M.cx) cell.M.ck)
 
@@ -36,8 +46,8 @@ let ind i = S.make (2 * i) ' '
 
 let out_cell och cell =
    let cc = border cell in
-   P.fprintf och "%s<td class=\"%s\">%s</td>\n"
-      (ind (i+4)) (S.concat " " cc) (key cell)
+   P.fprintf och "%s<td class=\"%s\"%s>%s</td>\n"
+      (ind (i+4)) (S.concat " " cc) (name cell) (key cell)
 
 let out_row och row =
    P.fprintf och "%s<tr>\n" (ind (i+3));
diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css
index 5897aedc6..7ee236c53 100644
--- a/helm/www/lambdadelta/css/ld_web.css
+++ b/helm/www/lambdadelta/css/ld_web.css
@@ -85,6 +85,20 @@ img.w3c {
    height: 32px; /* this should be 31px */
 }
 
+/* alignment ****************************************************************/
+
+td.top {
+   vertical-align: top;
+}
+
+td.middle {
+   vertical-align: middle;
+}
+
+td.bottom {
+   vertical-align: bottom;
+}
+
 /* background colors ********************************************************/
 
 .gray {
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 684c81c6c..680b83770 100644
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -234,6 +234,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 15:47:14 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 23:25:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 2520a4102..808aff0c9 100644
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -202,6 +202,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 16:13:35 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 23:25:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 8391452ae..8c30c357e 100644
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -302,6 +302,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 15:59:00 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 23:25:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html
index b76aab942..a96ad7126 100644
--- a/helm/www/lambdadelta/version_1.html
+++ b/helm/www/lambdadelta/version_1.html
@@ -186,6 +186,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 15:47:14 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 23:25:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html
index 8c71c51d8..0435540bf 100644
--- a/helm/www/lambdadelta/version_2.html
+++ b/helm/www/lambdadelta/version_2.html
@@ -151,6 +151,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 15:59:00 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 13 Jul 2014 23:25:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl
index 43e612301..2eef8f149 100644
--- a/helm/www/lambdadelta/xslt/ld_web_root.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl
@@ -118,6 +118,15 @@
    <span class="date"><xsl:value-of select="@date"/></span>
 </xsl:template>
 
+<xsl:template match="ld:basic-icon">
+   <img class="icon32"
+	alt="[basic lambdadelta]"
+	title="basic lambdadelta"
+	src="{$baseurl}images/basic_32.png"
+   />
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
 <xsl:template match="ld:footer">
    <xsl:call-template name="rule"/>
    <div class="spacer"><br/></div>