added html templates and pages

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

index 9cf2ca7f9fb5b4437345c57cd300355039460b8b..5b243e78362c30e52b1eb39c05a33f5fe87cbfc5 100644 (file)
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -73,24 +73,24 @@
  <xsl:template name="var_name">
   <xsl:param name="uri"/>
   <xsl:param name="string" select="&quot;&quot;"/>
-  <xsl:variable name="prefix" select="substring-before($uri, &quot; &quot;)"/>
+  <xsl:variable name="prefix0" select="substring-before($uri, &quot; &quot;)"/>
    <xsl:variable name="suffix" select="substring-after($uri, &quot; &quot;)"/> 
    <xsl:variable name="prefix">
     <xsl:call-template name="name_of_uri_bis">
-    <xsl:with-param name="uri" select="$prefix"/>
+    <xsl:with-param name="uri" select="$prefix0"/>
     </xsl:call-template>
    </xsl:variable> 
    <!--xsl:if test="string($prefix) != &quot; &quot; "-->
-   <xsl:variable name="string" select="concat($string,', ', $prefix)"/>
+   <xsl:variable name="string1" select="concat($string,', ', $prefix)"/>
    <!--/xsl:if-->
    <xsl:choose>
     <xsl:when test="$suffix = &quot;&quot;">
-   <xsl:value-of select="substring-after(concat($string, ' '),',')"/>
+   <xsl:value-of select="substring-after(concat($string1, ' '),',')"/>
     </xsl:when>
     <xsl:otherwise>
     <xsl:call-template name="var_name">
      <xsl:with-param name="uri" select="$suffix"/>
-    <xsl:with-param name="string" select="$string"/>
+    <xsl:with-param name="string" select="$string1"/>
     </xsl:call-template>
     </xsl:otherwise>
    </xsl:choose>
@@ -119,6 +119,8 @@
  </xsl:template>
  
  <xsl:template match="ConstantType" mode="noannot">
+    <xsl:variable name="ConstantBodyUrl" 
+                  select="concat($BaseCICURI,'.body')"/>
      <Definition name="{@name}" helm:xref="{@id}">  
       <xsl:if test="string(@params) != &quot;&quot;">
        <Params>
@@ -139,7 +141,9 @@
         </body>
        </xsl:otherwise>
       </xsl:choose> -->
-     <body/>
+     <body>
+      <m:ci definitionURL="{$ConstantBodyUrl}">click here</m:ci>
+     </body>
       <type>
         <xsl:apply-templates select="./*[1]"/>
       </type>
@@ -158,7 +162,9 @@
       <body>
        <xsl:apply-templates select="./*[1]"/>
       </body>
-     <type/>
+     <type>
+       <xsl:apply-templates select="document($ConstantTypeUrl)/*[1]/*[1]"/>
+     </type>
      </Definition>
  </xsl:template>
  
@@ -169,7 +175,7 @@
        <Conjecture no="{@no}" helm:xref="{@id}">
          <xsl:for-each select="*">
           <xsl:copy>
-          <xsl:copy-of select="@of"/>
+          <xsl:copy-of select="@name"/>
            <xsl:attribute name="helm:xref">
             <xsl:value-of select="@id"/>
            </xsl:attribute>
@@ -181,6 +187,9 @@
       <body>
         <xsl:apply-templates select="body/*[1]"/>
       </body>
+     <type>
+       <xsl:apply-templates select="document($ConstantTypeUrl)/*[1]/*[1]"/>
+     </type>
      </CurrentProof> 
  </xsl:template>