added LICENSE

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

index 6ad0a492274e7c67fb012f8b529067b5b3ff4023..333a1ef9b537ec0cea29c2a304907a73cd4169f8 100644 (file)
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -1,5 +1,29 @@
  <?xml version="1.0"?>
  
+<!-- Copyright (C) 2000, HELM Team                                     -->
+<!--                                                                   -->
+<!-- This file is part of HELM, an Hypertextual, Electronic            -->
+<!-- Library of Mathematics, developed at the Computer Science         -->
+<!-- Department, University of Bologna, Italy.                         -->
+<!--                                                                   -->
+<!-- HELM is free software; you can redistribute it and/or             -->
+<!-- modify it under the terms of the GNU General Public License       -->
+<!-- as published by the Free Software Foundation; either version 2    -->
+<!-- of the License, or (at your option) any later version.            -->
+<!--                                                                   -->
+<!-- HELM is distributed in the hope that it will be useful,           -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
+<!-- GNU General Public License for more details.                      -->
+<!--                                                                   -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software               -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
+<!-- MA  02111-1307, USA.                                              -->
+<!--                                                                   -->
+<!-- For details, see the HELM World-Wide-Web page,                    -->
+<!-- http://cs.unibo.it/helm/.                                         -->
+
  <!--******************************************************************--> 
  <!-- XSLT version 0.1 of CIC objects to objects and MathML content:   -->
  <!-- First draft: March 21 2000, Irene Schena                         -->
@@ -48,10 +72,10 @@
        </xsl:otherwise>
       </xsl:choose> -->
       <body>
-      <xsl:apply-templates select="body"/>
+      <xsl:apply-templates select="body/*"/>
       </body>
       <type>
-       <xsl:apply-templates select="type"/>
+       <xsl:apply-templates select="type/*"/>
       </type>
      </Definition> 
  </xsl:template>
@@ -64,7 +88,7 @@
        </Params>
       </xsl:if>
       <type>
-       <xsl:apply-templates select="type"/>
+       <xsl:apply-templates select="type/*"/>
       </type>
      </Axiom> 
  </xsl:template>
@@ -77,10 +101,10 @@
        </Conjecture>
       </xsl:for-each>
       <body>
-       <xsl:apply-templates select="body"/>
+       <xsl:apply-templates select="body/*"/>
       </body>
       <type>
-       <xsl:apply-templates select="type"/>
+       <xsl:apply-templates select="type/*"/>
       </type>
      </CurrentProof> 
  </xsl:template>
@@ -121,7 +145,7 @@
  <xsl:template match="Variable" mode="noannot"> 
      <Variable name="{@name}" helm:xref="{@id}">
       <type>
-       <xsl:apply-templates select="type"/>
+       <xsl:apply-templates select="type/*"/>
       </type>
      </Variable> 
  </xsl:template>
@@ -147,7 +171,7 @@
         <xsl:choose>
         <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
          <m:ci>
-         <xsl:value-of select="target/@binder"/>
+         <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> 
@@ -202,7 +226,7 @@
  <xsl:param name="noleft" select="0"/>
  <xsl:param name="number" select="1"/>
      <xsl:if test="$noleft != 0">
-     <m:ci>$<xsl:value-of select="$number"/></m:ci>
+     <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>