xmlns:m="http://www.w3.org/1998/Math/MathML"
xmlns:helm="http://www.cs.unibo.it/helm">
-<xsl:param name="type" select="0"/>
-<xsl:param name="getterURL" select="'http://localhost:8081/'"/>
-<xsl:variable name="absPath"><xsl:value-of select="$getterURL"/>getxml?uri=</xsl:variable>
-
<xsl:import href="objcontent.xsl"/>
-<xsl:include href="basic.xsl"/>
-<xsl:include href="set.xsl"/>
-<xsl:include href="reals.xsl"/>
+<xsl:include href="headercontent.xsl"/>
+<xsl:include href="getter.xsl"/>
+
+<xsl:param name="type" select="'standalone'"/>
+<xsl:param name="getterURL" select="'http://localhost:8081/'"/>
+<xsl:param name="CICURI" select="''"/>
<!-- CIC DEFINITION -->
-<xsl:template match="Definition">
- <xsl:choose>
- <xsl:when test="$type=0">
- <Definition name="{@name}" helm:xref="{@id}">
- <xsl:if test="string(@params) != """>
- <Params>
- <xsl:value-of select="@params"/>
- </Params>
- </xsl:if>
- <body>
- <xsl:apply-templates select="body/*[1]"/>
- </body>
+<xsl:template match="ConstantType">
+ <xsl:choose>
+ <xsl:when test="$type='typeonly'">
+ <type>
+ <xsl:apply-templates select="./*[1]" mode="noannot"/>
+ </type>
+ </xsl:when>
+ <xsl:otherwise>
+ <Definition name="{@name}" helm:xref="{@id}">
+ <xsl:if test="string(@params) != """>
+ <Params>
+ <xsl:call-template name="var_name">
+ <xsl:with-param name="uri" select="concat(@params, ' ')"/>
+ </xsl:call-template>
+ </Params>
+ </xsl:if>
+ <body/>
<type>
- <xsl:apply-templates select="type/*[1]"/>
+ <xsl:apply-templates select="./*[1]" mode="noannot"/>
</type>
</Definition>
- </xsl:when>
- <xsl:otherwise>
- <type>
- <xsl:apply-templates select="type/*[1]"/>
- </type>
</xsl:otherwise>
- </xsl:choose>
+ </xsl:choose>
</xsl:template>
<xsl:template match="Axiom|CurrentProof|InductiveDefinition|Variable">
<xsl:apply-templates select="." mode="noannot"/>
</xsl:template>
-<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX">
+<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate">
<m:math>
<xsl:apply-templates select="." mode="noannot"/>
</m:math>
</xsl:template>
-<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX" mode="noannot">
+<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate" mode="noannot">
<xsl:apply-templates select="." mode="pure"/>
</xsl:template>
projects / helm.git / blobdiff