lazily ==> call_by_name (since it is really a call_by_name!)

[helm.git] / helm / style / objtheorycontent.xsl
diff --git a/helm/style/objtheorycontent.xsl b/helm/style/objtheorycontent.xsl

index bc0292ff7fb7f8134846b7d201e5088744ec4b4b..5bad7e108109156abaa78a05e02ae0268902249e 100644 (file)
--- a/helm/style/objtheorycontent.xsl
+++ b/helm/style/objtheorycontent.xsl
@@ -33,51 +33,52 @@
                                xmlns:m="http://www.w3.org/1998/Math/MathML"
                                xmlns:helm="http://www.cs.unibo.it/helm">
  
-<xsl:param name="type" select="'standalone'"/>
-<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="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:template match="ConstantType">
+  <xsl:choose>
     <xsl:when test="$type='typeonly'">
      <type>
-     <xsl:apply-templates select="type/*[1]"/>
+     <xsl:apply-templates select="./*[1]" mode="noannot"/>
      </type>
     </xsl:when>
     <xsl:otherwise>
      <Definition name="{@name}" helm:xref="{@id}">  
       <xsl:if test="string(@params) != &quot;&quot;">
        <Params>
-       <xsl:value-of select="@params"/>
+       <xsl:call-template name="var_name">
+        <xsl:with-param name="uri" select="concat(@params, ' ')"/>
+       </xsl:call-template>
        </Params>
       </xsl:if>
-     <body>
-       <xsl:apply-templates select="body/*[1]"/>
-     </body>
+     <body/>
       <type>
-       <xsl:apply-templates select="type/*[1]"/>
+       <xsl:apply-templates select="./*[1]" mode="noannot"/>
       </type>
      </Definition>
     </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>