- better formatting/factorization of tables used for grammar description

- improved rendering toward TeX

diff --git a/matita/help/C/Makefile b/matita/help/C/Makefile
index 329473d06e0d0da4896eb07dc080b326db490f44..a25effd585339a680662dc6f9ec2f73fc19d638e 100644 (file)
--- a/matita/help/C/Makefile
+++ b/matita/help/C/Makefile
@@ -57,10 +57,10 @@ pdf-stamp: $(patsubst %.xml,%.pdf,$(MAIN))
 %.fo: %.xml
        xsltproc $(FO_XSL) $< | xmllint --format - > $@
 ifeq ($(TEX_METHOD),docbook2tex)
-%.tex: %.xml
+%.tex: %.xml $(DEPS)
        docbook2tex $<
 else ifeq ($(TEX_METHOD),xsl)
-%.tex: %.xml $(TEX_XSL)
+%.tex: %.xml $(TEX_XSL) $(DEPS)
        xsltproc $(TEX_XSL) $< > $@
 endif
 
@@ -77,6 +77,5 @@ endif
 %.ps: %.dvi
        dvips $<
 
-.PRECIOUS: matita.tex
-
+.PRECIOUS: matita.tex matita.dvi
 

diff --git a/matita/help/C/matita-tex.xsl b/matita/help/C/matita-tex.xsl
index 79a402178962c7471a133a3f9c39af3705563c24..5f51e7cbc00b65417288f9fdb9c9984ee4347689 100644 (file)
--- a/matita/help/C/matita-tex.xsl
+++ b/matita/help/C/matita-tex.xsl
@@ -10,5 +10,22 @@
   <xsl:param name="latex.book.preamble.post">\usepackage{txfonts}
 \SetUnicodeOption{mathletters} % prefer math-mode letters
 </xsl:param>
+  <xsl:param name="ulink.show">0</xsl:param>
+
+  <!-- proper alignment of tables used for grammars -->
+
+  <xsl:template match="tgroup[../@role='grammar']">
+    <xsl:text>\begin{tabular}{rcll}
+</xsl:text>
+    <xsl:apply-templates />
+    <xsl:text>\end{tabular}
+</xsl:text>
+  </xsl:template>
+
+  <xsl:template match="variablelist/title">
+    <xsl:text>\paragraph*{</xsl:text>
+    <xsl:apply-templates />
+    <xsl:text>} </xsl:text>
+  </xsl:template>
 
 </xsl:stylesheet>

diff --git a/matita/help/C/matita-xhtml.xsl b/matita/help/C/matita-xhtml.xsl
index e67b4897331a47aaa1095be8ec39aff51116542c..099c390f08b939b3164b042b43061c7160665dd3 100644 (file)
--- a/matita/help/C/matita-xhtml.xsl
+++ b/matita/help/C/matita-xhtml.xsl
@@ -7,6 +7,7 @@
 
   <xsl:param name="use.id.as.filename" select="1" />
   <xsl:param name="html.stylesheet">docbook.css</xsl:param>
+  <xsl:param name="table.borders.with.css" select="1" />
   <!--
   <xsl:param name="header.rule" select="0" />
   <xsl:param name="footer.rule" select="0" />

diff --git a/matita/help/C/matita.xml b/matita/help/C/matita.xml
index e32262ae44f7c7166b86390c541c42beca30661e..89d9ee658e579b276d84cc2f19c8e1b929c6b35e 100644 (file)
--- a/matita/help/C/matita.xml
+++ b/matita/help/C/matita.xml
@@ -24,19 +24,21 @@
       url='http://www.mysql.com'>MySQL</ulink> </application>">
 
   <!-- Entities for BNF -->
-  <!ENTITY id "<emphasis><link linkend='id'>id</link></emphasis>">
-  <!ENTITY uri "<emphasis><link linkend='uri'>uri</link></emphasis>">
-  <!ENTITY char "<emphasis><link linkend='char'>char</link></emphasis>">
-  <!ENTITY uri-step "<emphasis><link linkend='uri-step'>uri-step</link></emphasis>">
-  <!ENTITY nat "<emphasis><link linkend='nat'>nat</link></emphasis>">
-  <!ENTITY term "<emphasis><link linkend='term'>term</link></emphasis>">
-  <!ENTITY match_pattern "<emphasis><link linkend='match_pattern'>match_pattern</link></emphasis>">
-  <!ENTITY args "<emphasis><link linkend='args'>args</link></emphasis>">
-  <!ENTITY args2 "<emphasis><link linkend='args2'>args2</link></emphasis>">
-  <!ENTITY sterm "<emphasis><link linkend='sterm'>sterm</link></emphasis>">
-  <!ENTITY intros-spec "<emphasis><link linkend='intros-spec'>intros-spec</link></emphasis>">
-  <!ENTITY pattern "<emphasis><link linkend='pattern'>pattern</link></emphasis>">
-  <!ENTITY reduction-kind "<emphasis><link linkend='reduction-kind'>reduction-kind</link></emphasis>">
+  <!ENTITY id "<emphasis><link linkend='grammar.id'>id</link></emphasis>">
+  <!ENTITY uri "<emphasis><link linkend='grammar.uri'>uri</link></emphasis>">
+  <!ENTITY char "<emphasis><link linkend='grammar.char'>char</link></emphasis>">
+  <!ENTITY uri-step "<emphasis><link linkend='grammar.uri-step'>uri-step</link></emphasis>">
+  <!ENTITY nat "<emphasis><link linkend='grammar.nat'>nat</link></emphasis>">
+  <!ENTITY term "<emphasis><link linkend='grammar.term'>term</link></emphasis>">
+  <!ENTITY rec_def "<emphasis><link linkend='grammar.rec_def'>rec_def</link></emphasis>">
+  <!ENTITY match_pattern "<emphasis><link linkend='grammar.match_pattern'>match_pattern</link></emphasis>">
+  <!ENTITY match_branch "<emphasis><link linkend='grammar.match_branch'>match_branch</link></emphasis>">
+  <!ENTITY args "<emphasis><link linkend='grammar.args'>args</link></emphasis>">
+  <!ENTITY args2 "<emphasis><link linkend='grammar.args2'>args2</link></emphasis>">
+  <!ENTITY sterm "<emphasis><link linkend='grammar.sterm'>sterm</link></emphasis>">
+  <!ENTITY intros-spec "<emphasis><link linkend='grammar.intros-spec'>intros-spec</link></emphasis>">
+  <!ENTITY pattern "<emphasis><link linkend='grammar.pattern'>pattern</link></emphasis>">
+  <!ENTITY reduction-kind "<emphasis><link linkend='grammar.reduction-kind'>reduction-kind</link></emphasis>">
 ]>
 
 <?yelp:chunk-depth 3?>

diff --git a/matita/help/C/sec_install.xml b/matita/help/C/sec_install.xml
index be9ddaa11364bae4257f0ed3b13ce55ef7c9cba7..eb4cfb17e1e804f3405c0f9b16cba4d2b2cbadf1 100644 (file)
--- a/matita/help/C/sec_install.xml
+++ b/matita/help/C/sec_install.xml
@@ -274,57 +274,60 @@
        
       <para> Quite a few (optional) arguments may be passed to the
        <application>configure</application> command line to change build time
-       parameters. They are listed in the table below, together with their
-       default values.
+       parameters. They are listed below, together with their
+       default values: </para>
 
-       <table frame="all">
+       <variablelist>
          <title> <application>configure</application> command line
            arguments</title>
-         <tgroup cols="3" align="left" colsep="1" rowsep="1">
-           <thead>
-             <row>
-               <entry align="center">Argument</entry>
-               <entry align="center">Default</entry>
-               <entry align="center">Description</entry>
-             </row>
-           </thead>
-           <tbody>
-             <row>
-               <entry>
-                 <userinput>--with-runtime-dir=<replaceable>dir</replaceable></userinput>
-               </entry>
-               <entry> <filename>/usr/local/matita/</filename> </entry>
-               <entry> <para> Runtime base directory where all &appname; stuff
-                   (executables, configuration files, standard
-                   library, ...) will be installed </para> </entry>
-             </row>
-             <row>
-               <entry>
-                 <userinput>--with-dbhost=<replaceable>host</replaceable></userinput>
-               </entry>
-               <entry> localhost </entry>
-               <entry> <para>Default SQL server hostname. Will be used while
-                   building the standard library during the installation and to
-                   create the default &appname; configuration. May be changed
-                   later in configuration file.</para></entry>
-             </row>
-             <row>
-               <entry> <userinput>--enable-debug</userinput></entry>
-               <entry> disabled </entry>
-               <entry> <para> Enable debugging code. Not for the casual user.
-                 </para> </entry>
-             </row>
-           </tbody>
-         </tgroup>
-       </table>
 
-      </para>
+         <varlistentry>
+           <term>
+             <userinput>--with-runtime-dir=<replaceable>dir</replaceable></userinput>
+           </term>
+           <listitem>
+             <para>
+               (<emphasis>Default:</emphasis>
+               <filename>/usr/local/matita</filename>) Runtime base directory
+               where all &appname; stuff (executables, configuration files,
+               standard library, ...) will be installed
+             </para>
+           </listitem>
+         </varlistentry>
+
+         <varlistentry>
+           <term>
+             <userinput>--with-dbhost=<replaceable>host</replaceable></userinput>
+           </term>
+           <listitem>
+             <para>
+               (<emphasis>Default:</emphasis> localhost) Default SQL server
+               hostname. Will be used while building the standard library
+               during the installation and to create the default &appname;
+               configuration. May be changed later in configuration file.
+             </para>
+           </listitem>
+         </varlistentry>
+
+         <varlistentry>
+           <term>
+             <userinput>--enable-debug</userinput>
+           </term>
+           <listitem>
+             <para>
+               (<emphasis>Default:</emphasis> disabled) Enable debugging code.
+               Not for the casual user.
+             </para>
+           </listitem>
+         </varlistentry>
+       </variablelist>
 
       <para> Then you will manage the build and install process using
        <application><ulink type="http"
            url="http://www.gnu.org/software/make/">make</ulink></application>
        as usual. Below are reported the targets you have to invoke in sequence
-       to build and install.
+       to build and install:
+      </para>
 
        <variablelist>
          <title><application>make</application> targets</title>
@@ -357,8 +360,6 @@
          </varlistentry>
 
        </variablelist>
-
-      </para>
       
     </sect2>
 

diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml
index d2594c718ba2c35d753c3e4c9c6a1edb1ab04039..ab26aae4872f133d42ef74fcb32f3e389f9b32eb 100644 (file)
--- a/matita/help/C/sec_terms.xml
+++ b/matita/help/C/sec_terms.xml
@@ -26,78 +26,90 @@
   <title>Terms &amp; co.</title>
   <sect2 id="lexical">
   <title>Lexical conventions</title>
-  <para>
-    <table frame="all" rowsep="0" colsep="0">
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>id</title>
       <tgroup cols="4">
       <tbody>
        <row>
-       <entry id="id">&id;</entry>
+       <entry id="grammar.id">&id;</entry>
        <entry>::=</entry>
-        <entry><emphasis>〈〈any sequence of letters, underscores or valid <ulink url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink> prefixed by a latin letter ([a-zA-Z]) and post-fixed by a possible empty sequence of decorators ([?'`])〉〉</emphasis></entry>
+        <entry><emphasis>〈〈any sequence of letters, underscores or valid <ulink type="http" url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink> prefixed by a latin letter ([a-zA-Z]) and post-fixed by a possible empty sequence of decorators ([?'`])〉〉</emphasis></entry>
        </row>
       </tbody>
      </tgroup>
     </table>
-    <table frame="all" rowsep="0" colsep="0">
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>nat</title>
       <tgroup cols="4">
       <tbody>
        <row>
-       <entry id="nat">&nat;</entry>
+       <entry id="grammar.nat">&nat;</entry>
        <entry>::=</entry>
-       <entry><emphasis>〈〈any sequence of valid <ulink url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink></emphasis></entry>
+       <entry><emphasis>〈〈any sequence of valid <ulink type="http" url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink>〉〉</emphasis></entry>
        </row>
       </tbody>
      </tgroup>
     </table>
-    <table frame="all" rowsep="0" colsep="0">
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>char</title>
       <tgroup cols="4">
       <tbody>
        <row>
-       <entry id="char">&char;</entry>
+       <entry id="grammar.char">&char;</entry>
        <entry>::=</entry>
        <entry>[<emphasis role="bold">a</emphasis>-<emphasis role="bold">zA</emphasis>-<emphasis role="bold">Z0</emphasis>-<emphasis role="bold">9_-</emphasis>]</entry>
        </row>
       </tbody>
      </tgroup>
     </table>
-    <table frame="all" rowsep="0" colsep="0">
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>uri-step</title>
       <tgroup cols="4">
       <tbody>
        <row>
-       <entry id="uri-step">&uri-step;</entry>
+       <entry id="grammar.uri-step">&uri-step;</entry>
        <entry>::=</entry>
        <entry>&char;[&char;]…</entry>
        </row>
       </tbody>
      </tgroup>
     </table>
-    <table frame="all" rowsep="0" colsep="0">
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>uri</title>
       <tgroup cols="4">
       <tbody>
        <row>
-       <entry id="uri">&uri;</entry>
+       <entry id="grammar.uri">&uri;</entry>
        <entry>::=</entry>
        <entry>[<emphasis role="bold">cic:/</emphasis>|<emphasis role="bold">theory:/</emphasis>]&uri-step;[<emphasis role="bold">/</emphasis>&uri-step;]…<emphasis role="bold">.</emphasis>&id;[<emphasis role="bold">.</emphasis>&id;]…[<emphasis role="bold">#xpointer(</emphasis>&nat;<emphasis role="bold">/</emphasis>&nat;[<emphasis role="bold">/</emphasis>&nat;]…<emphasis role="bold">)</emphasis>]</entry>
        </row>
       </tbody>
      </tgroup>
     </table>
-  </para>
   </sect2>
   <sect2 id="terms">
   <title>Terms</title>
+
+  <!-- ZACK: Sample EBNF snippet, see:
+  http://www.docbook.org/tdg/en/html/productionset.html -->
+  <!--
+  <productionset>
+    <title>Terms</title>
+    <production id="grammar.term">
+      <lhs>&term;</lhs>
+      <rhs>&sterm;</rhs>
+      <lineannotation></lineannotation>
+    </production>
+  </productionset>
+  -->
+
   <para>
-  <table frame="all" rowsep="0" colsep="0">
+  <table frame="topbot" rowsep="0" colsep="0" role="grammar">
     <title>Terms</title>
     <tgroup cols="4">
     <tbody>
      <row>
-      <entry id="term">&term;</entry>
+      <entry id="grammar.term">&term;</entry>
       <entry>::=</entry>
       <entry>&sterm;</entry>
       <entry>simple or delimited term</entry>
@@ -141,11 +153,10 @@
      <row>
       <entry/>
       <entry>|</entry>
-      <entry><emphasis role="bold">let</emphasis>
-      [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
-      &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
-      [<emphasis role="bold">:</emphasis> &term;]
-      <emphasis role="bold">≝</emphasis> &term;
+      <entry>
+       <emphasis role="bold">let</emphasis>
+       [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
+       &rec_def;
       </entry>
       <entry>(co)recursive definitions</entry>
      </row>
@@ -153,10 +164,7 @@
       <entry/>
       <entry/>
       <entry>
-      [<emphasis role="bold">and</emphasis>
-      [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
-      [<emphasis role="bold">:</emphasis> &term;]
-      <emphasis role="bold">≝</emphasis> &term;]…
+      [<emphasis role="bold">and</emphasis> &rec_def;]…
       </entry>
       <entry/>
      </row>
@@ -174,16 +182,32 @@
       <entry>…</entry>
       <entry>user provided notation</entry>
      </row>
+      <row>
+       <entry id="grammar.rec_def">&rec_def;</entry>
+       <entry>::=</entry>
+       <entry>
+         &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]…
+       </entry>
+      </row>
+      <row>
+       <entry />
+       <entry />
+       <entry>
+         [<emphasis role="bold">on</emphasis> &nat;]
+         [<emphasis role="bold">:</emphasis> &term;]
+         <emphasis role="bold">≝</emphasis> &term;]
+       </entry>
+      </row>
     </tbody>
    </tgroup>
   </table>
 
-  <table frame="all" rowsep="0" colsep="0">
+  <table frame="topbot" rowsep="0" colsep="0" role="grammar">
     <title>Simple terms</title>
     <tgroup cols="4">
     <tbody>
      <row>
-      <entry id="sterm">&sterm;</entry>
+      <entry id="grammar.sterm">&sterm;</entry>
       <entry>::=</entry>
       <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
       <entry/>
@@ -252,11 +276,9 @@
       <entry/>
       <entry>
        <emphasis role="bold">[</emphasis> 
-       &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
-         [
-         <emphasis role="bold">|</emphasis>
-         &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
-         ]…<emphasis role="bold">]</emphasis> </entry>
+       &match_branch;[<emphasis role="bold">|</emphasis>&match_branch;]…
+       <emphasis role="bold">]</emphasis> 
+      </entry>
       <entry/>
      </row>
      <row>
@@ -275,12 +297,12 @@
    </tgroup>
   </table>
 
-  <table frame="all" rowsep="0" colsep="0">
+  <table frame="topbot" rowsep="0" colsep="0" role="grammar">
     <title>Arguments</title>
     <tgroup cols="4">
     <tbody>
      <row>
-      <entry id="args">&args;</entry>
+      <entry id="grammar.args">&args;</entry>
       <entry>::=</entry>
       <entry>
        <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
@@ -307,16 +329,8 @@
       <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
       <entry/>
      </row>
-    </tbody>
-   </tgroup>
-  </table>
-
-  <table frame="all" rowsep="0" colsep="0">
-    <title>Miscellaneous arguments</title>
-    <tgroup cols="4">
-    <tbody>
      <row>
-      <entry id="args2">&args2;</entry>
+      <entry id="grammar.args2">&args2;</entry>
       <entry>::=</entry>
       <entry>&id;</entry>
       <entry/>
@@ -331,12 +345,17 @@
    </tgroup>
   </table>
 
-  <table frame="all" rowsep="0" colsep="0">
+  <table frame="topbot" rowsep="0" colsep="0" role="grammar">
     <title>Pattern matching</title>
     <tgroup cols="4">
     <tbody>
+      <row>
+       <entry id="grammar.match_branch">&match_branch;</entry>
+       <entry>::=</entry>
+       <entry>&match_pattern; <emphasis role="bold">⇒</emphasis> &term;</entry>
+      </row>
      <row>
-      <entry id="match_pattern">&match_pattern;</entry>
+      <entry id="grammar.match_pattern">&match_pattern;</entry>
       <entry>::=</entry>
       <entry>&id;</entry>
       <entry>0-ary constructor</entry>
@@ -485,12 +504,12 @@
 
     <sect2 id="introsspec">
     <title>intros-spec</title>
-    <table frame="all" rowsep="0" colsep="0">
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>intros-spec</title>
       <tgroup cols="4">
       <tbody>
        <row>
-       <entry id="intros-spec">&intros-spec;</entry>
+       <entry id="grammar.intros-spec">&intros-spec;</entry>
        <entry>::=</entry>
         <entry>[&nat;] [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</entry>
        </row>
@@ -502,12 +521,12 @@
 
     <sect2 id="pattern">
     <title>pattern</title>
-    <table frame="all" rowsep="0" colsep="0">
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>pattern</title>
       <tgroup cols="4">
       <tbody>
        <row>
-       <entry id="pattern">&pattern;</entry>
+       <entry id="grammar.pattern">&pattern;</entry>
        <entry>::=</entry>
         <entry>&TODO;</entry>
        </row>
@@ -522,12 +541,12 @@
     <para>Reduction kinds are normalization functions that transform a term
      to a convertible but simpler one. Each reduction kind can be used both
      as a tactic argument and as a stand-alone tactic.</para>
-    <table frame="all" rowsep="0" colsep="0">
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>reduction-kind</title>
       <tgroup cols="4">
       <tbody>
        <row>
-       <entry id="reduction-kind">&reduction-kind;</entry>
+       <entry id="grammar.reduction-kind">&reduction-kind;</entry>
        <entry>::=</entry>
         <entry><emphasis role="bold">demodulate</emphasis></entry>
        </row>
@@ -553,8 +572,8 @@
         <entry/>
         <entry>|</entry>
         <entry><emphasis role="bold">unfold</emphasis> [&sterm;]</entry>
-        <entry>δ-reduces the constant or variable specified, or that
-         in head position if none is specified</entry>
+        <entry>δ-reduces the constant or variable if specified, or that
+         in head position</entry>
        </row>
        <row>
         <entry/>