From d42059631d57a1c2964240b9905b235e2a945fc1 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 9 Jun 2006 14:33:16 +0000
Subject: [PATCH] Lexical conventions documented.

---
 helm/software/matita/help/C/matita.xml    |  2 ++
 helm/software/matita/help/C/sec_terms.xml | 35 +++++++++++++++++++----
 2 files changed, 32 insertions(+), 5 deletions(-)

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index 8934ffffd..7b3b3d30c 100644
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -25,6 +25,8 @@
   <!-- 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>">
diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index fbf8dd4ef..f7991374c 100644
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -13,8 +13,9 @@
 	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.
+    <listitem><para>Repetitions of a sequence of elements are given by putting the
+    sequence in square brackets, that are followed by three dots. The empty
+    sequence is a valid repetition.
     E.g.: [<emphasis role="bold">and</emphasis> &term;]…</para></listitem>
   </orderedlist>
   <sect1 id="terms_and_co">
@@ -29,7 +30,7 @@
        <row>
 	<entry id="id">&id;</entry>
 	<entry>::=</entry>
-	<entry><emphasis>〈〈&TODO;〉〉</emphasis></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>
        </row>
       </tbody>
      </tgroup>
@@ -41,7 +42,31 @@
        <row>
 	<entry id="nat">&nat;</entry>
 	<entry>::=</entry>
-	<entry><emphasis>〈〈&TODO;〉〉</emphasis></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>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>char</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+	<entry id="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">
+      <title>uri-step</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+	<entry id="uri-step">&uri-step;</entry>
+	<entry>::=</entry>
+	<entry>&char;[&char;]…</entry>
        </row>
       </tbody>
      </tgroup>
@@ -53,7 +78,7 @@
        <row>
 	<entry id="uri">&uri;</entry>
 	<entry>::=</entry>
-	<entry><emphasis>〈〈&TODO;〉〉</emphasis></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>
-- 
2.39.2