Attempt to make our markup respect the docbook specification(!), major changes

required:
1) added <para> wrappers where missing
2) added titles to tables
3) removed empty <thead> elements
Point (3) make yelp now shows rules in tables used for syntax references. IMO
this not a good reason to have empty <thead> elements, since they violates the
docbook DTDs. Either yelp should be fixed to not ignore frame/rowsep/colsep
attributes (as it currently does) or we need to find a different markup for
displaying EBNF like grammars.

diff --git a/matita/help/C/sec_commands.xml b/matita/help/C/sec_commands.xml
index b1bada0fddb9a06c348d8739c3ff639750155fc7..b4a6c8007679700dc27686e6a1b5dbf8064acb79 100644 (file)
--- a/matita/help/C/sec_commands.xml
+++ b/matita/help/C/sec_commands.xml
@@ -2,6 +2,11 @@
 <!-- ============ Commands ====================== -->
 <chapter id="sec_commands">
  <title>Other commands</title>
- &TODO;
+ <sect1>
+   <title>Introduction</title>
+   <para>
+     &TODO;
+   </para>
+ </sect1>
 </chapter>
 

diff --git a/matita/help/C/sec_gettingstarted.xml b/matita/help/C/sec_gettingstarted.xml
index 886603ab2d3facc60b06691f1423a93ff3eb3945..5f9dda35a829d1a6ba7fc86093841f1740de8fe6 100644 (file)
--- a/matita/help/C/sec_gettingstarted.xml
+++ b/matita/help/C/sec_gettingstarted.xml
@@ -11,22 +11,22 @@
 
   <sect1 id="unicode">
    <title>How to type Unicode symbols</title>
-   Unicode characters can be typed in several ways:
+   <para>Unicode characters can be typed in several ways:</para>
     <itemizedlist>
-     <listitem>Using the &quot;Shift+Ctrl+Unicode code&quot; standard
-      Gnome shortcut. E.g. Shift+Ctrl+3a9 generates &quot;Ω&quot;.
+      <listitem><para>Using the &quot;Shift+Ctrl+Unicode code&quot; standard Gnome shortcut. E.g. Shift+Ctrl+3a9 generates &quot;Ω&quot;.</para>
      </listitem>
-     <listitem>Typing the ligature &quot;\name&quot; where &quot;name&quot;
+     <listitem><para>Typing the ligature &quot;\name&quot; where &quot;name&quot;
       is a standard Unicode or LaTeX name for the character. Pressing
       &quot;Alt+L&quot; just after the last character of the name converts
       the ligature to the Unicode symbol. This operation is
       not required since Matita understands also the &quot;\name&quot;
       sequences. E.g. &quot;\Omega&quot; followed by Alt+L generates
-      &quot;Ω&quot;.
+      &quot;Ω&quot;.</para>
      </listitem>
-     <listitem>Typing one of the following ligatures (and opzionally converting
-      the ligature to the Unicode character has described before):
-      &quot;:=&quot; (which stands for ≝); &quot;->&quot; (which stands for &quot;→&quot;); &quot;=>&quot; (which stands for &quot;⇒&quot;).
+     <listitem><para>Typing one of the following ligatures (and optionally
+         converting the ligature to the Unicode character has described before):
+         &quot;:=&quot; (which stands for ≝); &quot;->&quot; (which stands for
+         &quot;→&quot;); &quot;=>&quot; (which stands for &quot;⇒&quot;).</para>
      </listitem>
     </itemizedlist>
   </sect1>
@@ -66,33 +66,32 @@
      an action in the drop down menu right of it.</para>
     <sect3 id="locate">
      <title>Searching by name</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
     <sect3 id="hint">
      <title>List of lemmas that can be applied</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
     <sect3 id="match">
      <title>Searching by exact match</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
     <sect3 id="elim">
      <title>List of elimination principles for a given type</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
     <sect3 id="instance">
      <title>Searching by instantiation</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
    </sect2>
   </sect1>
   <sect1 id="authoring">
    <title>Authoring</title>
    <sect2 id="developments">
    <title>How to use developments</title>
-   &TODO;
-   </sect2>
-   &TODO;
-  </sect1>
+   <para>   &TODO;</para>
+ </sect2>
+ </sect1>
 </chapter>
 

diff --git a/matita/help/C/sec_intro.xml b/matita/help/C/sec_intro.xml
index a29b4960d1dede420648f00e6eb14720865b2ff5..773bda24ca7f86fe0e0cba580a3e5f6e103d6b98 100644 (file)
--- a/matita/help/C/sec_intro.xml
+++ b/matita/help/C/sec_intro.xml
@@ -5,43 +5,44 @@
   <title>Introduction</title>
   <sect1 id="Features">
     <title>Features</title>
-
-    <para>
-      <application>Matita</application> is an interactive theorem prover
+    <para><application>Matita</application> is an interactive theorem prover
       (or proof assistant) with the following characteristics:</para>
-
     <itemizedlist>
-     <listitem>It is based on a variant of the Calculus of (co)Inductive
-      Constructions (CIC). CIC is also the logic of the Coq proof assistant.
-     </listitem>
-     <listitem>It adopts a procedural proof language, but it has a new
-      set of small step tacticals that improve proof structuring and debugging.
-     </listitem>
-     <listitem>It has a stand-alone graphical user interface (GUI) inspired by
-      CtCoq/Proof General. The GUI is implemented according to the state
-      of the art. In particular:
-      <itemizedlist>
-       <listitem>It is based and fully integrated with Gtk/Gnome.</listitem>
-       <listitem>An on-line help can be browsed via the Gnome documentation
-        browser.</listitem>
-       <listitem>Mathematical formulae are rendered in two dimensional
-        notation via MathML and Unicode.</listitem>
-      </itemizedlist>
-     </listitem>
-     <listitem>It integrates advanced browsing and searching procedures.
-     </listitem>
-     <listitem>It allows the use of the typical ambiguous mathematical notation
-      by means of a disambiguating parser.
-     </listitem>
-     <listitem>It is compatible with the library of Coq (definitions and
-      proof objects).
-     </listitem>
+      <listitem>
+        <para>It is based on a variant of the Calculus of (co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.</para>
+      </listitem>
+      <listitem>
+        <para>It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.</para>
+      </listitem>
+      <listitem>
+        <para>It has a stand-alone graphical user interface (GUI) inspired by
+CtCoq/Proof General. The GUI is implemented according to the state
+of the art. In particular:</para>
+        <itemizedlist>
+          <listitem>
+            <para>It is based and fully integrated with Gtk/Gnome.</para>
+          </listitem>
+          <listitem>
+            <para>An on-line help can be browsed via the Gnome documentation browser.</para>
+          </listitem>
+          <listitem>
+            <para>Mathematical formulae are rendered in two dimensional notation via MathML and Unicode.</para>
+          </listitem>
+        </itemizedlist>
+      </listitem>
+      <listitem>
+        <para>It integrates advanced browsing and searching procedures.</para>
+      </listitem>
+      <listitem>
+        <para>It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.</para>
+      </listitem>
+      <listitem>
+        <para>It is compatible with the library of Coq (definitions and proof objects).</para>
+      </listitem>
     </itemizedlist>
   </sect1>
-
   <sect1 id="WrtCoq">
     <title>Matita vs Coq</title>
-
     <para>
       The system shares a common look&amp;feel with the Coq proof assistant
       and its graphical user interface. The two systems have the same logic,
@@ -50,38 +51,46 @@
       From the user point of view the main lacking features
       with respect to Coq are:
     </para>
-
     <itemizedlist>
-     <listitem>proof extraction;</listitem>
-     <listitem>an extensible language of tactics;</listitem>
-     <listitem>automatic implicit arguments;</listitem>
-     <listitem>several ad-hoc decision procedures;</listitem>
-     <listitem>several rarely used variants for most of the tactics;</listitem>
-     <listitem>sections and local variables. To maintain compatibility
-      with the library of Coq, theorems defined inside sections are abstracted
-      by name over the section variables; their instances are explicitly
-      applied to actual arguments by means of explicit named
-      substitutions.</listitem>
+      <listitem>
+        <para>proof extraction;</para>
+      </listitem>
+      <listitem>
+        <para>an extensible language of tactics;</para>
+      </listitem>
+      <listitem>
+        <para>automatic implicit arguments;</para>
+      </listitem>
+      <listitem>
+        <para>several ad-hoc decision procedures;</para>
+      </listitem>
+      <listitem>
+        <para>several rarely used variants for most of the tactics;</para>
+      </listitem>
+      <listitem>
+        <para>sections and local variables. To maintain compatibility with the library of Coq, theorems defined inside sections are abstracted by name over the section variables; their instances are explicitly applied to actual arguments by means of explicit named substitutions.</para>
+      </listitem>
     </itemizedlist>
-
     <para>
       Still from the user point of view, the main differences with respect
       to Coq are:
     </para>
-
     <itemizedlist>
-     <listitem>the language of tacticals that allows execution of partial
-      tactical application;</listitem>
-     <listitem>the unification of the concept of metavariable and existential
-      variable;</listitem>
-     <listitem>terms with subterms that cannot be inferred are always allowed
-      as arguments of tactics or other commands;</listitem>
-     <listitem>ambiguous terms are disambiguated by direct interaction
-      with the user;</listitem>
-     <listitem>theorems and definitions in the library are always accessible
-      without needing to require/include them; right now, only notation needs
-      to be included to become active, but we plan to remove this limitation.</listitem>
+      <listitem>
+        <para>the language of tacticals that allows execution of partial tactical application;</para>
+      </listitem>
+      <listitem>
+        <para>the unification of the concept of metavariable and existential variable;</para>
+      </listitem>
+      <listitem>
+        <para>terms with subterms that cannot be inferred are always allowed as arguments of tactics or other commands;</para>
+      </listitem>
+      <listitem>
+        <para>ambiguous terms are disambiguated by direct interaction with the user;</para>
+      </listitem>
+      <listitem>
+        <para>theorems and definitions in the library are always accessible without needing to require/include them; right now, only notation needs to be included to become active, but we plan to remove this limitation.</para>
+      </listitem>
     </itemizedlist>
-
   </sect1>
 </chapter>

diff --git a/matita/help/C/sec_tacticals.xml b/matita/help/C/sec_tacticals.xml
index 870feed7c510f755ebe99ed066fe86d68b975656..ea863605fb1db802ee410daf935c7a06d5f20a8d 100644 (file)
--- a/matita/help/C/sec_tacticals.xml
+++ b/matita/help/C/sec_tacticals.xml
@@ -2,6 +2,11 @@
 <!-- ============ Tacticals ====================== -->
 <chapter id="sec_tacticals">
  <title>Tacticals</title>
- &TODO;
+ <sect1>
+   <title>Introduction</title>
+   <para>
+     &TODO;
+   </para>
+ </sect1>
 </chapter>
 

diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml
index 6d359a7acbb57cae135060e8e690c4ea1d911b44..fbf8dd4ef9cb614c7dfb52eb4c2fa80e1ab210b2 100644 (file)
--- a/matita/help/C/sec_terms.xml
+++ b/matita/help/C/sec_terms.xml
@@ -5,62 +5,67 @@
   <title>Syntax</title>
   <para>To describe syntax in this manual we use the following conventions:</para>
   <orderedlist>
-   <listitem>Non terminal symbols are emphasized and have a link to their definition. E.g.: &term;</listitem>
-   <listitem>Terminal symbols are in bold. E.g.: <emphasis role="bold">theorem</emphasis></listitem>
-   <listitem>Optional sequences of elements are put in square brackets.
-    E.g.: [<emphasis role="bold">in</emphasis> &term;]</listitem>
-   <listitem>Alternatives are put in square brakets and they are separated
-    by vertical bars. E.g.: [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>]</listitem>
-   <listitem>Repetition of sequences of elements are given by putting the
+    <listitem><para>Non terminal symbols are emphasized and have a link to their
+       definition. E.g.: &term;</para></listitem>
+    <listitem><para>Terminal symbols are in bold. E.g.:
+       <emphasis role="bold">theorem</emphasis></para></listitem>
+    <listitem><para>Optional sequences of elements are put in square brackets.
+       E.g.: [<emphasis role="bold">in</emphasis> &term;]</para></listitem>
+    <listitem><para>Alternatives are put in square brakets and they are
+       separated by vertical bars. E.g.: [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>]</para></listitem>
+    <listitem><para>Repetition of sequences of elements are given by putting the
     first sequence in square brackets, that are followed by three dots.
-    E.g.: [<emphasis role="bold">and</emphasis> &term;]…</listitem>
+    E.g.: [<emphasis role="bold">and</emphasis> &term;]…</para></listitem>
   </orderedlist>
   <sect1 id="terms_and_co">
   <title>Terms &amp; co.</title>
   <sect2 id="lexical">
   <title>Lexical conventions</title>
-  <table>
-    <tgroup cols="4">
-     <thead />
-    <tbody>
-     <row>
-      <entry id="id">&id;</entry>
-      <entry>::=</entry>
-      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
-     </row>
-    </tbody>
-   </tgroup>
-  </table>
-  <table>
-    <tgroup cols="4">
-     <thead />
-    <tbody>
-     <row>
-      <entry id="nat">&nat;</entry>
-      <entry>::=</entry>
-      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
-     </row>
-    </tbody>
-   </tgroup>
-  </table>
-  <table>
-    <tgroup cols="4">
-     <thead />
-    <tbody>
-     <row>
-      <entry id="uri">&uri;</entry>
-      <entry>::=</entry>
-      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
-     </row>
-    </tbody>
-   </tgroup>
-  </table>
+  <para>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>id</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="id">&id;</entry>
+       <entry>::=</entry>
+       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>nat</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="nat">&nat;</entry>
+       <entry>::=</entry>
+       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>uri</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="uri">&uri;</entry>
+       <entry>::=</entry>
+       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+  </para>
   </sect2>
   <sect2 id="terms">
   <title>Terms</title>
-  <table>
+  <para>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Terms</title>
     <tgroup cols="4">
-     <thead />
     <tbody>
      <row>
       <entry id="term">&term;</entry>
@@ -144,9 +149,9 @@
    </tgroup>
   </table>
 
-  <table>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Simple terms</title>
     <tgroup cols="4">
-     <thead />
     <tbody>
      <row>
       <entry id="sterm">&sterm;</entry>
@@ -241,9 +246,9 @@
    </tgroup>
   </table>
 
-  <table>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Arguments</title>
     <tgroup cols="4">
-     <thead />
     <tbody>
      <row>
       <entry id="args">&args;</entry>
@@ -277,9 +282,9 @@
    </tgroup>
   </table>
 
-  <table>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Miscellaneous arguments</title>
     <tgroup cols="4">
-     <thead />
     <tbody>
      <row>
       <entry id="args2">&args2;</entry>
@@ -297,9 +302,9 @@
    </tgroup>
   </table>
 
-  <table>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Pattern matching</title>
     <tgroup cols="4">
-     <thead />
     <tbody>
      <row>
       <entry id="match_pattern">&match_pattern;</entry>
@@ -316,6 +321,7 @@
     </tbody>
    </tgroup>
   </table>
+  </para>
 
   </sect2>
   </sect1>

diff --git a/matita/help/C/sec_usernotation.xml b/matita/help/C/sec_usernotation.xml
index 92698f824e31b155c8e0d6644d6ac21c4ad311b8..dd1362d0200aa8cd64630b5428439e2db161e1ed 100644 (file)
--- a/matita/help/C/sec_usernotation.xml
+++ b/matita/help/C/sec_usernotation.xml
@@ -2,6 +2,11 @@
 <!-- ============ User Notation ====================== -->
 <chapter id="sec_usernotation">
  <title>Extending the syntax</title>
- &TODO;
+ <sect1>
+   <title>Introduction</title>
+   <para>
+     &TODO;
+   </para>
+ </sect1>
 </chapter>