]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/objcontent.xsl
Until Garrigue puts a META file in lablgtk, we can use this one.
[helm.git] / helm / style / objcontent.xsl
index 4ab19c854ba8aa8f59bd7a162e82f8e999e9b3d7..9b98250511fba36ef67907a29c777035ad1ab7ff 100644 (file)
 <xsl:template match="cicxml">
     <xsl:variable name="url"><xsl:value-of select="@baseurl"/></xsl:variable>
     <xsl:variable name="stylesheet"><xsl:value-of select="@stylesheet"/></xsl:variable>
+    <!--
     <xsl:processing-instruction name="cocoon-format">type="text/xml"</xsl:processing-instruction>
     <xsl:processing-instruction name="xml-stylesheet">href="<xsl:value-of select='concat($url,$stylesheet)'/>" type="text/xsl"</xsl:processing-instruction>
     <xsl:processing-instruction name="cocoon-process">type="xslt"</xsl:processing-instruction>
+    -->
     <xsl:apply-templates select="*[1]"/>
 </xsl:template>
 
       </xsl:otherwise>
      </xsl:choose> -->
      <body>
-      <xsl:apply-templates select="body/*"/>
+      <xsl:apply-templates select="body/*[1]"/>
      </body>
      <type>
-       <xsl:apply-templates select="type/*"/>
+       <xsl:apply-templates select="type/*[1]"/>
      </type>
     </Definition> 
 </xsl:template>
@@ -88,7 +90,7 @@
       </Params>
      </xsl:if>
      <type>
-       <xsl:apply-templates select="type/*"/>
+       <xsl:apply-templates select="type/*[1]"/>
      </type>
     </Axiom> 
 </xsl:template>
       </Conjecture>
      </xsl:for-each>
      <body>
-       <xsl:apply-templates select="body/*"/>
+       <xsl:apply-templates select="body/*[1]"/>
      </body>
      <type>
-       <xsl:apply-templates select="type/*"/>
+       <xsl:apply-templates select="type/*[1]"/>
      </type>
     </CurrentProof> 
 </xsl:template>
     <Variable name="{@name}" helm:xref="{@id}">
      <xsl:if test="name(*[1])='body'">
       <body>
-       <xsl:apply-templates select="body/*"/>
+       <xsl:apply-templates select="body/*[1]"/>
       </body>
      </xsl:if>
      <type>
-       <xsl:apply-templates select="type/*"/>
+       <xsl:apply-templates select="type/*[1]"/>
      </type>
     </Variable> 
 </xsl:template>
 
-<!--*******************************************-->
-<!--    ABSTRACTING PARAMETERS AND COUNTING    -->
-<!--*******************************************-->
-<!-- Si dimentica i CAST dei termini che astrae. Nel caso dell'astrazione -->
-<!-- dei lambda dei pattern del CASE, qualora i lambda non si trovino     -->
-<!-- nella forma weak-head, astrae solo i lambda che trova e restituisce  -->
-<!-- un corpo depurato da tutti i primi cast che precedono il termine     -->
-<!-- restituito.                                                          -->
-
-<xsl:template match="*" mode="abstparams">
-<xsl:param name="noparams" select="0"/>
-<xsl:param name="target" select="0"/>
-<xsl:param name="binder">PROD</xsl:param>
-    <xsl:choose>
-    <xsl:when test="($noparams != 0) and ((name(.)=string($binder)) or (name(.)=&quot;CAST&quot;))">
-     <xsl:choose>
-     <xsl:when test="name(.) = string($binder)">
-      <xsl:if test="$target = 0">
-       <xsl:choose>
-       <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
-        <m:ci>
-         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
-        </m:ci>
-       </xsl:when>
-       <xsl:otherwise> 
-        <Param name="{target/@binder}">
-         <xsl:apply-templates select="source" mode="noannot"/>
-        </Param>
-       </xsl:otherwise>
-       </xsl:choose>
-      </xsl:if>
-      <xsl:apply-templates select="target/*[1]" mode="abstparams">
-       <xsl:with-param name="noparams" select="$noparams - 1"/>
-       <xsl:with-param name="target" select="$target"/>
-       <xsl:with-param name="binder" select="$binder"/>
-      </xsl:apply-templates>
-     </xsl:when>
-     <xsl:otherwise>
-      <xsl:apply-templates select="term/*[1]" mode="abstparams">
-       <xsl:with-param name="noparams" select="$noparams"/>
-       <xsl:with-param name="target" select="$target"/>
-       <xsl:with-param name="binder" select="$binder"/>
-      </xsl:apply-templates>
-     </xsl:otherwise>
-     </xsl:choose>
-    </xsl:when>
-    <xsl:otherwise> 
-     <xsl:choose>
-     <xsl:when test="($target = 1) and ($noparams != 0)">
-      <m:apply>
-      <m:csymbol>app</m:csymbol>
-      <xsl:apply-templates select="." mode="noannot"/>
-      <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noparams"/></xsl:call-template>
-      </m:apply>
-     </xsl:when>
-     <xsl:otherwise>
-      <xsl:choose>
-      <xsl:when test="$noparams != 0">
-      <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noparams"/></xsl:call-template>
-      </xsl:when>
-      <xsl:otherwise>
-       <xsl:if test="$target = 1">
-        <xsl:apply-templates select="." mode="noannot"/>
-       </xsl:if>
-      </xsl:otherwise>
-      </xsl:choose>
-     </xsl:otherwise>
-     </xsl:choose>
-    </xsl:otherwise>
-    </xsl:choose>
-</xsl:template>
-
-<xsl:template name="printparam">
-<xsl:param name="noleft" select="0"/>
-<xsl:param name="number" select="1"/>
-    <xsl:if test="$noleft != 0">
-     <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value">$<xsl:value-of select="$number"/></xsl:with-param></xsl:call-template></m:ci>
-     <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noleft - 1"/><xsl:with-param name="number" select="$number + 1"/></xsl:call-template>  
-    </xsl:if>
-</xsl:template>
-
-<xsl:template match="*" mode="counting">
-<xsl:param name="noparams" select="0"/>
-<xsl:param name="count" select="0"/>
- <xsl:choose>
- <xsl:when test="name(.) = &quot;PROD&quot;">
-  <xsl:apply-templates select="target/*[1]" mode="counting">
-   <xsl:with-param name="noparams" select="$noparams"/>
-   <xsl:with-param name="count" select="$count + 1"/>
-  </xsl:apply-templates>
- </xsl:when>
- <xsl:when test="name(.) = &quot;CAST&quot;">
-  <xsl:apply-templates select="term/*[1]" mode="counting">
-   <xsl:with-param name="noparams" select="$noparams"/>
-   <xsl:with-param name="count" select="$count"/> 
-  </xsl:apply-templates>
- </xsl:when>
- <xsl:otherwise>
-  <xsl:value-of select="$count - $noparams"/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
 </xsl:stylesheet>