- xhtbl: we added the real concatenation of cells (without added spaces)

- web site: we added a page for each version of \lambda\delta

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 46a6259309141adec2ec3038a65f9876c75a7068..c3c16c3cbe4e04ff5dc4b49b614538631848a5fc 100644 (file)
--- 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, 06 Jul 2014 17:03:50 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 20:28:30 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 93b2272a4f86c5ee48871de49b4dcc20b2603d2c..9fc581eb9f9323556dc236ad97e45970e7392a11 100644 (file)
--- 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, 06 Jul 2014 17:03:50 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 20:28:30 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index e4bebe63d329ae164b9d9d163a45b06dd00128b6..3511fbfb0705ac2586194136823161960b181683 100644 (file)
--- 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, 06 Jul 2014 17:03:50 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 20:28:30 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/bin/xhtbl/textLexer.mll b/helm/www/lambdadelta/bin/xhtbl/textLexer.mll
index aa8f42fe4f14ef757fb3603caa425209e30afa6e..4b06e4c402f61044f1f17a99c2713e41fa1e45c2 100644 (file)
--- a/helm/www/lambdadelta/bin/xhtbl/textLexer.mll
+++ b/helm/www/lambdadelta/bin/xhtbl/textLexer.mll
@@ -22,6 +22,7 @@ rule token = parse
    | "["      { out "["; TP.OB                  }
    | "]"      { out "]"; TP.CB                  }   
    | "*"      { out "*"; TP.SR                  }
+   | "^"      { out "^"; TP.CF                  }
    | "+"      { out "+"; TP.PS                  }
    | "("      { out "("; TP.OP                  }
    | ")"      { out ")"; TP.CP                  }   

diff --git a/helm/www/lambdadelta/bin/xhtbl/textParser.mly b/helm/www/lambdadelta/bin/xhtbl/textParser.mly
index 3dba122d04a9581cec3008d3c396245aced8a8f9..5873959881170bb78d3b98b0caee7e5794944542 100644 (file)
--- a/helm/www/lambdadelta/bin/xhtbl/textParser.mly
+++ b/helm/www/lambdadelta/bin/xhtbl/textParser.mly
@@ -20,7 +20,7 @@ let mk_string_atom s rs =
 
 %token <int> NUM
 %token <string> TEXT 
-%token SPACE NAME TABLE CSS URI EXT SR OC CC OB CB PS OP CP AT EOF
+%token SPACE NAME TABLE CSS URI EXT SR OC CC OB CB PS CF OP CP AT EOF
 
 %start script
 %type <(string * string) list * (string * Table.table * Table.css Attr.atoms * Table.uri Attr.atoms * Table.ext Attr.atoms) list> script
@@ -45,8 +45,9 @@ text:
 ;
 
 texts:
-  | text          { [$1]     }
-  | text PS texts { $1 :: $3 }
+  | text          { [$1]                    }
+  | text PS texts { $1 :: T.Plain " " :: $3 }
+  | text CF texts { $1 :: $3                }
 ;
 
 key:

diff --git a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml
index ece6949d920814fb15059a1431b66e182281797a..339a9aeecfc58c33da0ccf09268dfa4dab413582 100644 (file)
--- a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml
@@ -50,7 +50,7 @@ let text = function
    | T.Link (false, uri, s) -> P.sprintf "@@(\"%s\" \"%s\")" uri s
 
 let key = function
-   | T.Text sl       -> S.concat " + " (L.map text sl)
+   | T.Text sl       -> S.concat " ^ " (L.map text sl)
    | T.Glue None     -> "*"
    | T.Glue (Some i) -> P.sprintf "%u" i
 

diff --git a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml
index 603c7f1bebd1baa2706ce4273b34e5a214ccc5b3..e46682c3f13bd8930379a2738d25d652e8dde476 100644 (file)
--- a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml
+++ b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml
@@ -30,7 +30,7 @@ let text baseuri ext = function
       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.cu cell.M.cx) 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/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 9b799f06056adf21f588b0fa8d55336b38e6121b..e79359b0de77f561c270737438eaa1525f49a423 100644 (file)
--- 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, 06 Jul 2014 17:03:50 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 20:28:30 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 0fb9ca8e2ffeb23323f944a3b4841a51e507d99b..cd48d35d4c1fe2d24dac1b2f0930c013d05095c4 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -79,7 +79,9 @@
           </tr>
           <tr>
             <td class="snns orange">2</td>
-            <td class="snnn orange">basic_2</td>
+            <td class="snnn orange">
+              <a href="http://lambdadelta.info/version_2.html">basic_2</a>
+            </td>
             <td class="snnn orange">
               <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>
             </td>
@@ -90,7 +92,9 @@
           </tr>
           <tr>
             <td class="snss red">1</td>
-            <td class="snsn red">basic_1</td>
+            <td class="snsn red">
+              <a href="http://lambdadelta.info/version_1.html">basic_1</a>
+            </td>
             <td class="snsn red">
               <a href="http://coq.inria.fr/">Coq 7.3.1</a>
             </td>
@@ -139,6 +143,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 17:03:50 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Jul 2014 20:28:30 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html
new file mode 100644 (file)
index 0000000..5bf4e0a
--- /dev/null
+++ b/helm/www/lambdadelta/version_1.html
@@ -0,0 +1,136 @@
+<?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 λδ version 1</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 class="snss component sky">
+              <a href="http://lambdadelta.info/index.html">foreword</a>
+            </td>
+            <td class="snss component magenta">
+              <a href="http://lambdadelta.info/news.html">news</a>
+            </td>
+            <td class="snss component orange">
+              <a href="http://lambdadelta.info/documentation.html">documentation</a>
+            </td>
+            <td class="ssss component green">
+              <a href="http://lambdadelta.info/implementation.html">implementation</a>
+            </td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
+
+   <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="foreword">Formats <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 specification of λδ version 1
+      is available in the following formats:
+      <ul>
+        <li>
+         <a href="http://lambdadelta.info/download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</a>
+         (revised <span class="date">2012-10</span>).
+         Source scripts.
+         <a href="http://lambdadelta.info/implementation.html#bibtex">BibTeX entry</a>
+      </li>
+      </ul>
+      <ul>
+        <li>
+         <a href="http://lambdadelta.info/static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5"</a>
+         (revised <span class="date">2011-09</span>).
+         Static HTML pages generated by the <a href="http://helm.cs.unibo.it/">HELM</a> rendering engine.  
+         <ul>
+            <li>
+               <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
+                  Confluence of reduction</a>
+               (Church-Rosser property).
+            </li>
+            <li>
+               <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
+                  Correctness of types</a>.
+            </li>
+            <li>
+               <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
+                  Uniqueness of types up to conversion</a>.
+            </li>
+            <li>
+               <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
+                  Subject reduction of the type assignment</a>.
+            </li>
+            <li>
+               <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
+                  Strong normalization of the typed terms</a>.
+            </li>
+            <li>
+               <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
+                  Decidability of the type inference problem</a>.
+            </li>
+         </ul>
+      </li>
+      </ul>
+      <ul>
+        <li>
+         <a href="http://mowgli.cs.unibo.it:58080/apply?keys=RT&amp;xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&amp;prop.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.thencoding=UTF-8&amp;prop.encoding=UTF-8&amp;prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=UTF-8&amp;param.media-type=text/html&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;profile=default&amp;param.profile=default&amp;param.CICURI=theory:/matita/lambdadelta/">
+            lambdadelta_1 for Matita 0.5"</a>
+         (revised <span class="date">2011-09</span>).
+         <a href="http://helm.cs.unibo.it/">HELM</a> directory.
+         <span class="date">Notice: the HELM rendering engine is offline.</span>
+      </li>
+      </ul>
+   </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="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 20:36:00 +0200</div>
+</body>
+</html>

diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html
new file mode 100644 (file)
index 0000000..27030b1
--- /dev/null
+++ b/helm/www/lambdadelta/version_2.html
@@ -0,0 +1,93 @@
+<?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 λδ version 2</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 class="snss component sky">
+              <a href="http://lambdadelta.info/index.html">foreword</a>
+            </td>
+            <td class="snss component magenta">
+              <a href="http://lambdadelta.info/news.html">news</a>
+            </td>
+            <td class="snss component orange">
+              <a href="http://lambdadelta.info/documentation.html">documentation</a>
+            </td>
+            <td class="ssss component green">
+              <a href="http://lambdadelta.info/implementation.html">implementation</a>
+            </td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
+
+   <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="foreword">Formats <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
+    </div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      The formal specification of λδ version 2
+      is available in the following formats:
+      <ul>
+        <li>
+         <a href="http://lambdadelta.info/download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</a>
+         (revised <span class="date">2014-07</span>).
+         Source scripts.
+         <a href="http://lambdadelta.info/implementation.html#bibtex">BibTeX entry</a>
+      </li>
+      </ul>
+   </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="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 20:36:00 +0200</div>
+</body>
+</html>

diff --git a/helm/www/lambdadelta/web/home/version_1.ldw.xml b/helm/www/lambdadelta/web/home/version_1.ldw.xml
new file mode 100644 (file)
index 0000000..4c75421
--- /dev/null
+++ b/helm/www/lambdadelta/web/home/version_1.ldw.xml
@@ -0,0 +1,62 @@
+<?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 λδ version 1"
+>
+   <sitemap name="sitemap"/>
+
+   <section9 name="foreword">Formats</section9>
+   <body>
+      The formal specification of λδ version 1
+      is available in the following formats:
+      <topitem>
+         <rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
+         (revised <date date="2012-10"/>).
+         Source scripts.
+         <rlink to="implementation.html#bibtex">BibTeX entry</rlink>
+      </topitem>
+      <topitem>
+         <rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5"</rlink>
+         (revised <date date="2011-09"/>).
+         Static HTML pages generated by the <link to="http://helm.cs.unibo.it/">HELM</link> rendering engine.  
+         <list>
+            <item>
+               <rlink to="static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
+                  Confluence of reduction</rlink>
+               (Church-Rosser property).
+            </item>
+            <item>
+               <rlink to="static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
+                  Correctness of types</rlink>.
+            </item>
+            <item>
+               <rlink to="static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
+                  Uniqueness of types up to conversion</rlink>.
+            </item>
+            <item>
+               <rlink to="static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
+                  Subject reduction of the type assignment</rlink>.
+            </item>
+            <item>
+               <rlink to="static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
+                  Strong normalization of the typed terms</rlink>.
+            </item>
+            <item>
+               <rlink to="static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
+                  Decidability of the type inference problem</rlink>.
+            </item>
+         </list>
+      </topitem>
+      <topitem>
+         <link to="http://mowgli.cs.unibo.it:58080/apply?keys=RT&amp;xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&amp;prop.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.thencoding=UTF-8&amp;prop.encoding=UTF-8&amp;prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=UTF-8&amp;param.media-type=text/html&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;profile=default&amp;param.profile=default&amp;param.CICURI=theory:/matita/lambdadelta/">
+            lambdadelta_1 for Matita 0.5"</link>
+         (revised <date date="2011-09"/>).
+         <link to="http://helm.cs.unibo.it/">HELM</link> directory.
+         <date date="Notice: the HELM rendering engine is offline."/>
+      </topitem>
+   </body>
+
+   <footer/>
+</page>

diff --git a/helm/www/lambdadelta/web/home/version_2.ldw.xml b/helm/www/lambdadelta/web/home/version_2.ldw.xml
new file mode 100644 (file)
index 0000000..8da683d
--- /dev/null
+++ b/helm/www/lambdadelta/web/home/version_2.ldw.xml
@@ -0,0 +1,23 @@
+<?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 λδ version 2"
+>
+   <sitemap name="sitemap"/>
+
+   <section4 name="foreword">Formats</section4>
+   <body>
+      The formal specification of λδ version 2
+      is available in the following formats:
+      <topitem>
+         <rlink to="download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</rlink>
+         (revised <date date="2014-07"/>).
+         Source scripts.
+         <rlink to="implementation.html#bibtex">BibTeX entry</rlink>
+      </topitem>
+   </body>
+
+   <footer/>
+</page>

diff --git a/helm/www/lambdadelta/web/home/versions.tbl b/helm/www/lambdadelta/web/home/versions.tbl
index 900b281c8612bb3549da7f3e0fd4fc951098cade..590c8e11c421b954832e52d6fd9345dcbf762f4d 100644 (file)
--- a/helm/www/lambdadelta/web/home/versions.tbl
+++ b/helm/www/lambdadelta/web/home/versions.tbl
@@ -6,13 +6,14 @@ table {
         "started" "announced" "released" "dismissed"
       ] 
    class "orange" 
-      [ "2" "basic_2" @("http://matita.cs.unibo.it/" "Matita 0.99.2")
+      [ "2" @@("version_2" "basic_2") @("http://matita.cs.unibo.it/" "Matita 0.99.2")
         "April 2011" "July 2014" "Planned in 2014" "Not planned yet"
       ] 
    class "red"
-      [ "1" "basic_1" @("http://coq.inria.fr/" "Coq 7.3.1")
+      [ "1" @@("version_1" "basic_1") @("http://coq.inria.fr/" "Coq 7.3.1")
         "May 2004" "January 2006" "November 2006" "May 2008" ] 
 }
 
 class "component" [ 0 ]
 
+ext ".html" { 1 }

diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl
index 20e35cf632339b0e31791a423530bcd56cec9644..a2bb7d14dd01e409496243987a1905cbaab08753 100644 (file)
--- a/helm/www/lambdadelta/xslt/ld_web_root.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl
@@ -58,16 +58,10 @@
    </div>
 </xsl:template>
 
-<xsl:template match="ld:link">
-   <a href="{@to}">
-      <xsl:apply-templates/>
-   </a>
-</xsl:template>
-
-<xsl:template match="ld:rlink">
-   <a href="{$baseurl}{@to}">
+<xsl:template match="ld:topitem">
+   <ul><li>
       <xsl:apply-templates/>
-   </a>
+   </li></ul>
 </xsl:template>
 
 <xsl:template match="ld:news">
@@ -90,6 +84,30 @@
    </div>
 </xsl:template>
 
+<xsl:template match="ld:link">
+   <a href="{@to}">
+      <xsl:apply-templates/>
+   </a>
+</xsl:template>
+
+<xsl:template match="ld:rlink">
+   <a href="{$baseurl}{@to}">
+      <xsl:apply-templates/>
+   </a>
+</xsl:template>
+
+<xsl:template match="ld:list">
+   <ul><xsl:apply-templates/></ul>
+</xsl:template>
+
+<xsl:template match="ld:item">
+   <li><xsl:apply-templates/></li>
+</xsl:template>
+
+<xsl:template match="ld:date">
+   <span class="date"><xsl:value-of select="@date"/></span>
+</xsl:template>
+
 <xsl:template match="ld:footer">
    <xsl:call-template name="rule"/>
    <div class="spacer"><br/></div>