documentation for the inline command

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index f66e6409336fd7698ed8d88f3acd3217e7f690c7..aa45a806a5f02b05125d3339cdc0c5542d421ff8 100644 (file)
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -55,6 +55,8 @@
   <!ENTITY autoparams "<emphasis><link linkend='grammar.autoparams'>auto_params</link></emphasis>">
   <!ENTITY justification "<emphasis><link linkend='grammar.justification'>justification</link></emphasis>">
   <!ENTITY simpleautoparam "<emphasis><link linkend='grammar.simpleautoparam'>simple_auto_param</link></emphasis>">
+  <!ENTITY inlineparams "<emphasis><link linkend='grammar.inlineparams'>inline_params</link></emphasis>">  
+  <!ENTITY inlineparam "<emphasis><link linkend='grammar.inlineparam'>inline_param</link></emphasis>">  
   <!ENTITY interpretation_argument "<emphasis><link linkend='grammar.interpretation_argument'>interpretation_argument</link></emphasis>">
   <!ENTITY interpretation_rhs "<emphasis><link linkend='grammar.interpretation_rhs'>interpretation_rhs</link></emphasis>">
   <!ENTITY csymbol "<emphasis><link linkend='grammar.csymbol'>csymbol</link></emphasis>">

diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml
index 19685bf9034e167fd0f4744501dd8ad390a3b7a6..7e22f33043d39ec5e0fcb62e7ce0c20ca1e41593 100644 (file)
--- a/helm/software/matita/help/C/sec_commands.xml
+++ b/helm/software/matita/help/C/sec_commands.xml
@@ -379,7 +379,7 @@
  </sect1>
  <sect1 id="command_qed">
    <title>qed</title>
-   <para><userinput></userinput></para>
+   <para><userinput>qed</userinput></para>
    <para>
      <variablelist>
        <varlistentry>
@@ -401,5 +401,188 @@
      </variablelist>
    </para>
  </sect1>
-</chapter>
+ 
+ <sect1 id="command_inline">
+   <title>inline</title>
+   <para><userinput>inline &quot;s&quot; params</userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry>
+         <term>Synopsis:</term>
+         <listitem>
+           <para>
+            <emphasis role="bold">inline</emphasis> &qstring; &inlineparams;
+           </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>Inlines a representation of the item <command>s</command>,
+which can be the URI of a HELM object. If an entire HELM directory (i.e. a base
+URI) or the path of a *.ma source file is provided, all the contained objects
+are represented in a row.
+If the inlined object has a proof, this proof is represented in several ways
+depending on the provided parameters.</para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
+   </para>
+   
+    <sect2 id="inline-params">
+    <title>inline-params</title>
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>inline-params</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="grammar.inlineparams">&inlineparams;</entry>
+       <entry>::=</entry>
+        <entry>[&inlineparam; [&inlineparam;] … ]</entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>inline-param</title>
+      <tgroup cols="4">
+      <tbody>
+       
+       <row>
+       <entry id="grammar.inlineparam">&inlineparam;</entry>
+       <entry>::=</entry>
+       <entry><emphasis role="bold">axiom</emphasis></entry>
+        <entry>Try to give an <link linkend="axiom">axiom</link> flavour
+           (bodies are omitted even if present) 
+       </entry>
+       </row>
+
+       <row>
+        <entry/>
+        <entry>|</entry>       
+       <entry><emphasis role="bold">definition</emphasis></entry>
+        <entry>Try give a <link linkend="definition">definition</link> flavour
+       </entry>
+       </row>
+
+       <row>
+        <entry/>
+        <entry>|</entry>       
+       <entry><emphasis role="bold">theorem</emphasis></entry>
+        <entry>Try give a <link linkend="theorem">theorem</link> flavour
+       </entry>
+       </row>
+
+       <row>
+        <entry/>
+        <entry>|</entry>       
+       <entry><emphasis role="bold">lemma</emphasis></entry>
+        <entry>Try give a <link linkend="lemma">lemma</link> flavour
+       </entry>
+       </row>
+
+       <row>
+        <entry/>
+        <entry>|</entry>       
+       <entry><emphasis role="bold">remark</emphasis></entry>
+        <entry>Try give a <link linkend="remark">remark</link> flavour
+       </entry>
+       </row>
 
+       <row>
+        <entry/>
+        <entry>|</entry>       
+       <entry><emphasis role="bold">fact</emphasis></entry>
+        <entry>Try give a <link linkend="fact">fact</link> flavour
+       </entry>
+       </row>
+
+       <row>
+        <entry/>
+        <entry>|</entry>       
+       <entry><emphasis role="bold">variant</emphasis></entry>
+        <entry>Try give a <link linkend="variant">variant</link> flavour
+              (implies <emphasis role="bold">plain</emphasis>)
+       </entry>
+       </row>
+
+       <row>
+        <entry/>
+        <entry>|</entry>       
+       <entry><emphasis role="bold">declarative</emphasis></entry>
+        <entry>Represent proofs using 
+           <link linkend="sec_declarative_tactics">declarative tactics</link>
+          (this is the dafault and can be omitted)
+       </entry>
+       </row>
+       
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">procedural</emphasis></entry>
+        <entry>Represent proofs using 
+           <link linkend="sec_tactics">procedural tactics</link>
+               </entry>
+       </row>
+       
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">plain</emphasis></entry>
+        <entry>Represent proofs using plain 
+          <link linkend="tbl_terms">proof terms</link>
+       </entry>
+       </row>
+
+       <row>
+        <entry/>
+        <entry>|</entry>
+       <entry><emphasis role="bold">nodefaults</emphasis></entry>
+        <entry>
+        Do not use the tactics depending on the
+        <link linkend="command_default">default</link> command
+          (<link linkend="tac_rewrite">rewrite</link>
+           in the <emphasis role="bold">procedural</emphasis> mode)
+       </entry>
+       </row>
+
+       <row valign="top">
+        <entry/>
+        <entry>|</entry>
+       <entry><emphasis role="bold">level=&nat;</emphasis></entry>
+        <entry>
+        Set the level of the procedural proof representation
+        (the default is the highest level)
+         <itemizedlist>
+          <listitem>
+          Tactics used at level 1:
+           <link linkend="tac_exact">exact</link>
+         </listitem>
+          <listitem>
+          Additional tactics used at level 2:
+           <link linkend="tac_letin">letin</link>,
+           <link linkend="tac_cut">cut</link>,
+           <link linkend="tac_change">change</link>,
+           <link linkend="tac_intros">intros</link>,
+           <link linkend="tac_apply">apply</link>,
+           <link linkend="tac_elim">elim</link>,
+           <link linkend="tac_cases">cases</link>,
+           <link linkend="tac_rewrite">rewrite</link>
+          </listitem>
+         </itemizedlist>
+       </entry>
+       </row>
+
+       <row>
+        <entry/>
+        <entry>|</entry>
+       <entry><emphasis role="bold">depth=&nat;</emphasis></entry>
+        <entry>&TODO;</entry>
+       </row>
+      
+      </tbody>
+     </tgroup>
+    </table>
+    </sect2>   
+ </sect1>
+</chapter>

diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index 2a42fc88d8d9039d4fe310ecee95f29ad1bb74fe..a1353b2f021aac59be2fe0896c2fbd827ab2795d 100644 (file)
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -140,7 +140,7 @@
   -->
 
   <para>
-  <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+  <table id="tbl_terms" frame="topbot" rowsep="0" colsep="0" role="grammar">
     <title>Terms</title>
     <tgroup cols="4">
     <tbody>