]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/content_to_html.xsl
----------------------------------------------------------------------
[helm.git] / helm / style / content_to_html.xsl
index fdf9b7829e3a5970d623ea95ca4f12ed23476849..1211e4881be96e555eba8e9d9245832cff02fdb8 100644 (file)
    <xsl:variable name="name">
     <xsl:value-of select="m:csymbol"/>
    </xsl:variable>
+   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
    <xsl:choose>
     <!-- FORALL -->
     <xsl:when test="$name='forall'">
        <xsl:apply-templates select="*[3]" mode="inline"/>
        <xsl:text>[</xsl:text>
        <xsl:apply-templates select="*[4]" mode="inline"/>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[2]" mode="inline"/>
        <xsl:text>]</xsl:text>
       </xsl:when>
        <SUB>
        <xsl:apply-templates select="*[3]" mode="inline"/>
        </SUB>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+         <a href="{$uri}">
+          <xsl:call-template name="mksymbol-1">
+           <xsl:with-param name="symbol" select="$name"/>
+           <xsl:with-param name="color" select="'green'"/>
+           <xsl:with-param name="size" select="'+0'"/>
+          </xsl:call-template>
+         </a>
+       </xsl:when>
+       <xsl:otherwise>
+          <xsl:call-template name="mksymbol-1">
+           <xsl:with-param name="symbol" select="$name"/>
+           <xsl:with-param name="color" select="'green'"/>
+           <xsl:with-param name="size" select="'+0'"/>
+          </xsl:call-template>
+       </xsl:otherwise>
+       </xsl:choose>
        <SUP>
        <xsl:apply-templates select="*[4]" mode="inline"/>
        </SUP>
       </xsl:when>
 
       <xsl:when test="$name='lift'">
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+       </xsl:otherwise>
+       </xsl:choose>
        <SUP>
        <xsl:apply-templates select="*[2]" mode="inline"/>
        </SUP>
       <!-- reduction --> 
       <xsl:when test="$name='beta_red1'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       <SUB>
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="'beta'"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       </SUB>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         </SUB>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         </SUB>
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>
 
       <xsl:when test="$name='beta_red'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       <SUB>
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="'beta'"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-        <xsl:text>*</xsl:text>
-       </SUB>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''"> 
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <xsl:text>*</xsl:text>
+         </SUB>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <xsl:text>*</xsl:text>
+         </SUB>
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>
 
       <xsl:when test="$name='par_beta_red1'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       <SUB>
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="'beta'"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       </SUB>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         </SUB>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         </SUB>
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>
 
       <xsl:when test="$name='par_beta_red'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       <SUB>
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="'beta'"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-        <xsl:text>*</xsl:text>
-       </SUB>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <xsl:text>*</xsl:text>
+         </SUB>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <xsl:text>*</xsl:text>
+         </SUB>
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>
 
       <!-- forgetful -->
       <xsl:when test="$name='forgetful'">
-       <a href="{*[1]/@definitionURL}">|</a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">|</a>
+       </xsl:when>
+       <xsl:otherwise>
+        |
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[2]" mode="inline"/>
-       <a href="{*[1]/@definitionURL}">|</a>
+        <xsl:choose>
+        <xsl:when test="$uri != ''">
+         <a href="{$uri}">|</a>
+        </xsl:when>
+       <xsl:otherwise>
+        |
+       </xsl:otherwise>
+       </xsl:choose>
       </xsl:when>
  
       <!-- boolean algebra of redexes -->
       <!-- isomorphic -->
       <xsl:when test="$name='isomorphic'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>
 
   </xsl:variable>
      <!-- <xsl:value-of select="$current_indent"/> -->
      <!-- <xsl:value-of select="$charlength"/> -->
+  <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
      <xsl:choose>
      <!-- FORALL -->
       <xsl:when test="$name='forall'">
        <xsl:apply-templates select="*[3]"/>
        <xsl:text>[</xsl:text>
        <xsl:apply-templates select="*[4]"/>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'blue'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'blue'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'blue'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[2]"/>
        <xsl:text>]</xsl:text>
       </xsl:when>
        <SUB>
        <xsl:apply-templates select="*[3]" mode="inline"/>
        </SUB>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+       </xsl:otherwise>
+       </xsl:choose>
        <SUP>
        <xsl:apply-templates select="*[4]" mode="inline"/>
        </SUP>
       </xsl:when>
 
       <xsl:when test="$name='lift'">
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+       </xsl:otherwise>
+       </xsl:choose>
        <SUP>
        <xsl:apply-templates select="*[2]" mode="inline"/>
        </SUP>
       <!-- reduction --> 
       <xsl:when test="$name='beta_red1'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       <SUB>
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="'beta'"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       </SUB>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         </SUB>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         </SUB>
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>
  
       <xsl:when test="$name='beta_red'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       <SUB>
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="'beta'"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-        <xsl:text>*</xsl:text>
-       </SUB>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <xsl:text>*</xsl:text>
+         </SUB>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <xsl:text>*</xsl:text>
+         </SUB>
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>
 
       <xsl:when test="$name='par_beta_red1'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       <SUB>
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="'beta'"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       </SUB>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         </SUB>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         </SUB>
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>
 
       <xsl:when test="$name='par_beta_red'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       <SUB>
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="'beta'"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-        <xsl:text>*</xsl:text>
-       </SUB>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <xsl:text>*</xsl:text>
+         </SUB>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <SUB>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="'beta'"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+         <xsl:text>*</xsl:text>
+         </SUB>
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>
 
       <!-- forgetful -->
       <xsl:when test="$name='forgetful'">
-       <a href="{*[1]/@definitionURL}">|</a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">|</a>
+       </xsl:when>
+       <xsl:otherwise>
+        |
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[2]" mode="inline"/>
-       <a href="{*[1]/@definitionURL}">|</a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">|</a>
+       </xsl:when>
+       <xsl:otherwise>
+        |
+       </xsl:otherwise>
+       </xsl:choose>
       </xsl:when>
  
       <!-- boolean algebra of redexes -->
       <!-- isomorphic -->
       <xsl:when test="$name='isomorphic'">
        <xsl:apply-templates select="*[2]" mode="inline"/>
-       <a href="{*[1]/@definitionURL}">
-        <xsl:call-template name="mksymbol-1">
-         <xsl:with-param name="symbol" select="$name"/>
-         <xsl:with-param name="color" select="'green'"/>
-         <xsl:with-param name="size" select="'+0'"/>
-        </xsl:call-template>
-       </a>
+       <xsl:choose>
+       <xsl:when test="$uri != ''">
+        <a href="{$uri}">
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+        </a>
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:call-template name="mksymbol-1">
+          <xsl:with-param name="symbol" select="$name"/>
+          <xsl:with-param name="color" select="'green'"/>
+          <xsl:with-param name="size" select="'+0'"/>
+         </xsl:call-template>
+       </xsl:otherwise>
+       </xsl:choose>
        <xsl:apply-templates select="*[3]" mode="inline"/>
       </xsl:when>