From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 20 Jun 2008 12:02:13 +0000 (+0000)
Subject: Further documentation for notation.
X-Git-Tag: make_still_working~5007
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5591e27a010ba6eb06cbd61b5b22358f2d572871;p=helm.git

Further documentation for notation.
---

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index 21dd9bc7b..1e45ce844 100644
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -60,8 +60,11 @@
   <!ENTITY csymbol "<emphasis><link linkend='grammar.csymbol'>csymbol</link></emphasis>">
   <!ENTITY usage "<emphasis><link linkend='grammar.usage'>usage</link></emphasis>">
   <!ENTITY notation_lhs "<emphasis><link linkend='grammar.notation_lhs'>notation_lhs</link></emphasis>">
+  <!ENTITY layout "<emphasis><link linkend='grammar.layout'>layout</link></emphasis>">
+  <!ENTITY literal "<emphasis><link linkend='grammar.literal'>literal</link></emphasis>">
   <!ENTITY notation_rhs "<emphasis><link linkend='grammar.notation_rhs'>notation_rhs</link></emphasis>">
   <!ENTITY associativity "<emphasis><link linkend='grammar.associativity'>associativity</link></emphasis>">
+  <!ENTITY symbol "<emphasis><link linkend='grammar.symbol'>symbol</link></emphasis>">
 ]>
 
 <?yelp:chunk-depth 3?>
diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index 082a5bb75..287267bd6 100644
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -109,7 +109,19 @@
        </row>
       </tbody>
       </tgroup>
-     </table>
+    </table>
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>symbol</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.symbol">&symbol;</entry>
+        <entry>::=</entry>
+        <entry><emphasis role="bold">〈〈None of the above〉〉</emphasis></entry>
+       </row>
+      </tbody>
+      </tgroup>
+    </table>
   </sect2>
   <sect2 id="terms">
   <title>Terms</title>
diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml
index 46bf146c9..734e95692 100644
--- a/helm/software/matita/help/C/sec_usernotation.xml
+++ b/helm/software/matita/help/C/sec_usernotation.xml
@@ -118,12 +118,187 @@
        <row>
         <entry id="grammar.notation_lhs">&notation_lhs;</entry>
         <entry>::=</entry>
-        <entry>&TODO;</entry>
-        <entry>&TODO;</entry>
+        <entry>&layout; [&layout;]…</entry>
        </row>
       </tbody>
       </tgroup>
-     </table>
+    </table>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>layout</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.layout">&layout;</entry>
+        <entry>::=</entry>
+        <entry>&layout; <emphasis role="bold">\sub</emphasis> &layout;</entry>
+        <entry>Subscript</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&layout; <emphasis role="bold">\sup</emphasis> &layout;</entry>
+        <entry>Superscript</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&layout; <emphasis role="bold">\below</emphasis> &layout;</entry>
+        <entry></entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&layout; <emphasis role="bold">\above</emphasis> &layout;</entry>
+        <entry></entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&layout; <emphasis role="bold">\over</emphasis> &layout;</entry>
+        <entry></entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&layout; <emphasis role="bold">\atop</emphasis> &layout;</entry>
+        <entry></entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">\frac</emphasis> &layout; &layout;</entry>
+        <entry>Fraction</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">\sqrt</emphasis> &layout;</entry>
+        <entry>Square root</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">\root</emphasis> &layout; <emphasis role="bold">\of</emphasis> &layout;</entry>
+        <entry>Generalized root</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">hbox</emphasis> <emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
+        <entry>Horizontal box</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">vbox</emphasis> <emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
+        <entry>Vertical box</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">hvbox</emphasis> <emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
+        <entry>Horizontal and vertical box</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">hovbox</emphasis> <emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
+        <entry>Horizontal or vertical box</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">break</emphasis></entry>
+        <entry>Breakable space</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
+        <entry>Group</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&id;</entry>
+        <entry>Placeholder for a term with no explicit precedence</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">term</emphasis> &nat; &id;</entry>
+        <entry>Placeholder for a term with explicit expected precedence</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">number</emphasis> &id;</entry>
+        <entry>Placeholder for a natural number</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">ident</emphasis> &id;</entry>
+        <entry>Placeholder for an identifier</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&literal;</entry>
+        <entry>Literal</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">opt</emphasis> &layout;</entry>
+        <entry>Optional layout (it can be omitted for parsing)</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">list0</emphasis> &layout;
+               [<emphasis role="bold">sep</emphasis> &literal;]</entry>
+        <entry>List of layouts separated by <command>sep</command> (default:
+               any blank)</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">list1</emphasis> &layout;
+               [<emphasis role="bold">sep</emphasis> &literal;]</entry>
+        <entry>Non empty list of layouts separated by <command>sep</command>
+               (default: any blank)</entry>
+       </row>
+      </tbody>
+      </tgroup>
+    </table>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>literal</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.literal">&literal;</entry>
+        <entry>::=</entry>
+        <entry>&symbol;</entry>
+        <entry>Unicode symbol</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&nat;</entry>
+        <entry>Natural number (a constant)</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">&apos;</emphasis>&id;<emphasis role="bold">&apos;</emphasis></entry>
+        <entry>New keyword for the lexer</entry>
+       </row>
+      </tbody>
+      </tgroup>
+    </table>
 
         </listitem>
       </varlistentry>