From ade543268430b595a7aef9fd14c19e2b1d22770d Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 12 Jul 2006 13:13:26 +0000
Subject: [PATCH] First skeleton of documentation for "other commands".

---
 helm/software/matita/help/C/matita.xml        |   2 +
 helm/software/matita/help/C/sec_commands.xml  | 239 +++++++++++++++++-
 helm/software/matita/help/C/sec_terms.xml     |  12 +
 .../matita/help/C/sec_usernotation.xml        |   3 +
 4 files changed, 251 insertions(+), 5 deletions(-)

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index 98d6489f3..8a9aee15e 100644
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -46,6 +46,8 @@
   <!ENTITY proofstep "<emphasis><link linkend='grammar.proofstep'>proof-step</link></emphasis>">
   <!ENTITY tactic "<emphasis><link linkend='grammar.tactic'>tactic</link></emphasis>">
   <!ENTITY LCFtactical "<emphasis><link linkend='grammar.LCFtactical'>LCF-tactical</link></emphasis>">
+  <!ENTITY string "<emphasis><link linkend='grammar.string'>string</link></emphasis>">
+  <!ENTITY interpretation "<emphasis><link linkend='grammar.interpretation'>interpretation</link></emphasis>">
 ]>
 
 <?yelp:chunk-depth 3?>
diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml
index 243960cf9..0ea8c06f9 100644
--- a/helm/software/matita/help/C/sec_commands.xml
+++ b/helm/software/matita/help/C/sec_commands.xml
@@ -2,15 +2,244 @@
 <!-- ============ Commands ====================== -->
 <chapter id="sec_commands">
  <title>Other commands</title>
- <sect1>
-   <title>Introduction</title>
+ <sect1 id="command_alias">
+   <title>alias</title>
+   <para><userinput>alias id &quot;s&quot; = &quot;def&quot;</userinput></para>
+   <para><userinput>alias symbol &quot;s&quot; (instance n) = &quot;def&quot;</userinput></para>
+   <para><userinput>alias num (instance n) = &quot;def&quot;</userinput></para>
    <para>
-     &TODO;
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">alias</emphasis>
+            [<emphasis role="bold">id</emphasis> <emphasis role="bold">&quot;</emphasis>&string;<emphasis role="bold">&quot;</emphasis> <emphasis role="bold">=</emphasis> <emphasis role="bold">&quot;</emphasis>&string;<emphasis role="bold">&quot;</emphasis>
+            | <emphasis role="bold">symbol</emphasis> <emphasis role="bold">&quot;</emphasis>&string;<emphasis role="bold">&quot;</emphasis> [<emphasis role="bold">(instance</emphasis> &nat;<emphasis role="bold">)</emphasis>] <emphasis role="bold">=</emphasis> <emphasis role="bold">&quot;</emphasis>&string;<emphasis role="bold">&quot;</emphasis>
+            | <emphasis role="bold">num</emphasis> [<emphasis role="bold">(instance</emphasis> &nat;<emphasis role="bold">)</emphasis>] <emphasis role="bold">=</emphasis> <emphasis role="bold">&quot;</emphasis>&string;<emphasis role="bold">&quot;</emphasis>
+            ]
+           </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>Used to give an hint to the disambiguating parser.
+            When the parser is faced to the identifier (or symbol)
+            <command>s</command> or to any number, it will prefer
+            interpretations that &quot;map <command>s</command> (or the
+            number) to <command>def</command>&quot;. For identifiers,
+            &quot;def&quot; is the URI of the interpretation.
+            E.g.: <command>cic:/matita/nat/nat.ind#xpointer(1/1/1)</command>
+            for the first constructor of the first inductive type defined
+            in the block of inductive type(s)
+            <command>cic:/matita/nat/nat.ind</command>.
+            For symbols and numbers, &quot;def&quot; is the label used to
+            mark the wanted
+            <link linkend="interpretation">interpretation</link>.
+           </para>
+          <para>When a symbol or a number occurs several times in the
+           term to be parsed, it is possible to give an hint only for the
+           instance <command>n</command>. When the instance is omitted,
+           the hint is valid for every occurrence.
+          </para>
+          <para>
+           Hints are automatically inserted in the script by Matita every
+           time the user is interactively asked a question to disambiguate
+           a term. This way the user won't be posed the same question twice
+           when the script will be executed again.</para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
+   </para>
+ </sect1>
+ <sect1 id="command_check">
+   <title>check</title>
+   <para><userinput></userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">check</emphasis>
+           </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>&TODO;</para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
+   </para>
+ </sect1>
+ <sect1 id="command_coercion">
+   <title>coercion</title>
+   <para><userinput></userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">coercion</emphasis>
+           </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>&TODO;</para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
+   </para>
+ </sect1>
+ <sect1 id="command_default">
+   <title>default</title>
+   <para><userinput></userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">default</emphasis>
+           </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>&TODO;</para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
+   </para>
+ </sect1>
+ <sect1 id="command_hint">
+   <title>hint</title>
+   <para><userinput></userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">hint</emphasis>
+           </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>&TODO;</para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
+   </para>
+ </sect1>
+ <sect1 id="command_include">
+   <title>include</title>
+   <para><userinput></userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">include</emphasis>
+           </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>&TODO;</para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
+   </para>
+ </sect1>
+ <sect1 id="command_include_first">
+   <title>include'</title>
+   <para><userinput></userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">include'</emphasis>
+           </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>&TODO;</para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
+   </para>
+ </sect1>
+ <sect1 id="command_set">
+   <title>set</title>
+   <para><userinput></userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">set</emphasis>
+           </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>&TODO;</para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
+   </para>
+ </sect1>
+ <sect1 id="command_whelp">
+   <title>whelp</title>
+   <para><userinput></userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">whelp</emphasis>
+           </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>&TODO;</para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
    </para>
  </sect1>
  <sect1 id="command_qed">
-   <title>Qed</title>
-   <para>&TODO;</para>
+   <title>qed</title>
+   <para><userinput></userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">qed</emphasis>
+           </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>&TODO;</para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
+   </para>
  </sect1>
 </chapter>
 
diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index 945a43837..a44131ebd 100644
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -26,6 +26,18 @@
   <title>Terms &amp; co.</title>
   <sect2 id="lexical">
   <title>Lexical conventions</title>
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>string</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+	<entry id="grammar.string">&string;</entry>
+	<entry>::=</entry>
+        <entry><emphasis>〈〈any sequence of characters excluded &quot;〉〉</emphasis></entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>id</title>
       <tgroup cols="4">
diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml
index dd1362d02..5956cf51c 100644
--- a/helm/software/matita/help/C/sec_usernotation.xml
+++ b/helm/software/matita/help/C/sec_usernotation.xml
@@ -7,6 +7,9 @@
    <para>
      &TODO;
    </para>
+   <para id="interpretation">
+     interpretation: &TODO;
+   </para>
  </sect1>
 </chapter>
 
-- 
2.39.2