From 3802156c428a73566ba757d7ec97ecc60697a2d6 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 20 Jun 2008 16:19:16 +0000
Subject: [PATCH] More documentation for notation.

---
 helm/software/matita/help/C/matita.xml        |   3 +
 .../matita/help/C/sec_usernotation.xml        | 132 ++++++++++++++++++
 2 files changed, 135 insertions(+)

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index 1e45ce844..a24b969eb 100644
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -65,6 +65,9 @@
   <!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>">
+  <!ENTITY level2_meta "<emphasis><link linkend='grammar.level2_meta'>level2_meta</link></emphasis>">
+  <!ENTITY unparsed_ast "<emphasis><link linkend='grammar.unparsed_ast'>unparsed_ast</link></emphasis>">
+  <!ENTITY unparsed_meta "<emphasis><link linkend='grammar.unparsed_meta'>unparsed_meta</link></emphasis>">
 ]>
 
 <?yelp:chunk-depth 3?>
diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml
index 734e95692..33c10c6f6 100644
--- a/helm/software/matita/help/C/sec_usernotation.xml
+++ b/helm/software/matita/help/C/sec_usernotation.xml
@@ -104,7 +104,139 @@
        <row>
         <entry id="grammar.notation_rhs">&notation_rhs;</entry>
         <entry>::=</entry>
+        <entry>&unparsed_ast;</entry>
         <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&unparsed_meta;</entry>
+        <entry>&TODO;</entry>
+       </row>
+      </tbody>
+      </tgroup>
+     </table>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>unparsed_ast</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.unparsed_ast">&unparsed_ast;</entry>
+        <entry>::=</entry>
+        <entry><emphasis role="bold">@{</emphasis>&term;<emphasis role="bold">}</emphasis></entry>
+        <entry>A content level AST (a term which is parsed, but not disambiguated).</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">@</emphasis>&id;</entry>
+        <entry><command>@id</command> is just an abbreviation for <command>@{id}</command></entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">@</emphasis>&csymbol;</entry>
+        <entry><command>@'symbol</command> is just an abbreviation for <command>@{'symbol}</command></entry>
+       </row>
+      </tbody>
+      </tgroup>
+     </table>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>unparsed_meta</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.unparsed_meta">&unparsed_meta;</entry>
+        <entry>::=</entry>
+        <entry><emphasis role="bold">${</emphasis>&level2_meta;<emphasis role="bold">}</emphasis></entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">$</emphasis>&id;</entry>
+        <entry><command>$id</command> is just an abbreviation for <command>${id}</command></entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">$</emphasis><emphasis role="bold">_</emphasis></entry>
+        <entry><command>$_</command> is just an abbreviation for <command>${_}</command></entry>
+       </row>
+      </tbody>
+      </tgroup>
+     </table>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>level2_meta</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.level2_meta">&level2_meta;</entry>
+        <entry>::=</entry>
+        <entry>&unparsed_ast;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">term</emphasis> &nat; &id;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">number</emphasis> &id;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">ident</emphasis> &id;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">fresh</emphasis> &id;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">anonymous</emphasis></entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&id;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">fold</emphasis> [<emphasis role="bold">left</emphasis>|<emphasis role="bold">right</emphasis>] &level2_meta; <emphasis role="bold">rec</emphasis> &id; &level2_meta;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">default</emphasis> &level2_meta; &level2_meta;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">if</emphasis> &level2_meta; <emphasis role="bold">then</emphasis> &level2_meta; <emphasis role="bold">else</emphasis> &level2_meta;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">fail</emphasis></entry>
         <entry>&TODO;</entry>
        </row>
       </tbody>
-- 
2.39.2