From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 7 May 2009 14:30:26 +0000 (+0000)
Subject: documentation for the inline command
X-Git-Tag: make_still_working~4013
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8caf14a7b9765bea19cf4249530a537fe6fe8d6e;p=helm.git

documentation for the inline command
---

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index f66e64093..aa45a806a 100644
--- 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 19685bf90..7e22f3304 100644
--- 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 2a42fc88d..a1353b2f0 100644
--- 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>