]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/content.xsl
Brand new implementation based on functors taking a strategy in input.
[helm.git] / helm / style / content.xsl
index 9aea96b3c5fa41b239b1a5c3c82881ca42c90f9b..e4712613802889706116468f0ebbab55ec97ecfc 100644 (file)
@@ -88,11 +88,13 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
 
 
 <xsl:template match="LETIN" mode="pure">
-       <xsl:apply-templates select="*[1]" mode="letin"/>
+       <xsl:apply-templates select="*[1]" mode="letin_pure"/>
 </xsl:template>
 
+<!-- Andrea: mode letin already exists in proofs.xsl, with a 
+    different meaning -->
 
-<xsl:template match="def" mode="letin">        
+<xsl:template match="def" mode="letin_pure">   
     <m:apply helm:xref="{@id}">
      <m:csymbol>let_in</m:csymbol>
      <m:bvar>
@@ -101,12 +103,12 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
       </m:ci>
      </m:bvar>
      <xsl:apply-templates select="*[1]" mode="noannot"/>
-     <xsl:apply-templates select="following-sibling::*[1]" mode="letin"/>
+     <xsl:apply-templates select="following-sibling::*[1]" mode="letin_pure"/>
     </m:apply>
 </xsl:template>
 
 
-<xsl:template match="target" mode="letin">
+<xsl:template match="target" mode="letin_pure">
        <xsl:apply-templates select="*[1]" mode="noannot"/>
 </xsl:template>
 
@@ -326,7 +328,22 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
         <m:csymbol>inst</m:csymbol>
         <xsl:apply-templates mode="noannot" select="*[1]" />
         <xsl:for-each select="arg">
-         <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:call-template name="name_of_uri"><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:with-param></xsl:call-template></m:ci>
+          <xsl:variable name="base_path">
+           <xsl:call-template name="path">
+            <xsl:with-param name="uri" select="../*[1]/@uri"/>
+           </xsl:call-template>
+          </xsl:variable>
+          <xsl:variable name="varUri" select="concat($base_path,@relUri)"/>
+         <m:ci definitionURL="{$varUri}">
+           <xsl:call-template name="insert_subscript">
+            <xsl:with-param name="node_value">
+             <xsl:call-template name="name_of_uri">
+              <xsl:with-param name="uri" select="$varUri"/>
+              <xsl:with-param name="extension" select="'.var'"/>
+             </xsl:call-template>
+            </xsl:with-param>
+           </xsl:call-template>
+          </m:ci>
          <xsl:apply-templates mode ="noannot" select="*[1]" />
         </xsl:for-each>
        </m:apply>