<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+<xsl:import href="utils.xsl"/>
+
<xsl:output method="html" encoding="iso-8859-1"/>
<!-- uri must end with '/' -->
<img border="0" src="{concat($interfaceURL,'/icons/',$icon)}" alt="[{$alt}]"/>
</td>
<td>
-<!-- Substituted with next lines to avoid Mozilla 0.8 bug setting this.search
- <a
- onClick=
- "top.{$target}uri='{$uri}';
- refresh{$target}Header('{$interfaceURL}/html/library/header.html');
- this.search='?keys={$keys}' +
- '&xmluri=' + escape('{$getterURL}ls?format=xml'+'&baseuri={$uri}')+
- '&param.uri={$uri}' +
- '&param.keys={$keys}' +
- '&param.getterURL={$getterURL}' +
- '&param.target={$target}' +
- '&param.interfaceURL={$interfaceURL}';"
- onMouseOver="window.status='{$uri}'; return true"
- href="apply"
- ><xsl:value-of select="$basename"/></a>
--->
+ <xsl:variable name="quoteduri">
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="$uri"/>
+ </xsl:call-template>
+ </xsl:variable>
<a
onClick=
- "top.{$target}uri='{$uri}';
+ "top.{$target}uri='{$quoteduri}';
refresh{$target}Header('{$interfaceURL}/html/library/header.html');
var search='?keys={$keys}' +
- '&xmluri=' + escape('{$getterURL}ls?format=xml'+'&baseuri={$uri}')+
- '&param.uri={$uri}' +
+ '&xmluri=' + escape('{$getterURL}ls?format=xml'+'&baseuri={$quoteduri}')+
+ '&param.uri={$quoteduri}' +
'&param.keys={$keys}' +
'&param.getterURL={$getterURL}' +
'&param.target={$target}' +
'&param.interfaceURL={$interfaceURL}';
+ var pathname = this.pathname;
+ if (pathname.charAt(0) != '/')
+ pathname = '/' + pathname;
this.href=
- this.protocol + '//' + this.host + this.pathname + search + this.hash;"
- onMouseOver="window.status='{$uri}'; return true"
+ this.protocol + '//' + this.host + pathname + search + this.hash;"
+ onMouseOver="window.status='{$quoteduri}'; return true"
href="apply"
><xsl:value-of select="$basename"/></a>
</td>
<xsl:variable name="name" select="@name"/>
<xsl:variable name="ann" select="ann/@value"/>
<xsl:variable name="types" select="types/@value"/>
+ <xsl:variable name="body" select="body/@value"/>
+ <xsl:variable name="proof_tree" select="proof_tree/@value"/>
<xsl:variable name="icon">
<xsl:choose>
<xsl:when test="$ann = 'YES'">text.gif</xsl:when>
<img border="0" src="{concat($interfaceURL,'/icons/',$icon)}" alt="[{@name}]"/>
</td>
<td>
+ <xsl:variable name="quoteduri">
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="$uri"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="quotedname">
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="$name"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="quotedbodyname">
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="concat($name,'.body')"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="quotedprooftreename">
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="concat($name,'.proof_tree')"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:value-of select="$name"/>
+ <xsl:text> </xsl:text>
<a href="" target="{$target}"
- onClick="this.href=makeURL('{$target}','{concat($uri,$name)}','{$ann}','{$types}')"
- onMouseOver="window.status='{concat($uri,$name)}'; return true"
- ><xsl:value-of select="$name"/></a>
+ onClick="this.href=makeURL('{$target}','{concat($quoteduri,$quotedname)}','{$ann}','{$types}')"
+ onMouseOver="window.status='{concat($quoteduri,$quotedname)}'; return true"
+ >
+ <xsl:choose>
+ <xsl:when test="not($body='NO')">Statement</xsl:when>
+ <xsl:otherwise>Definition</xsl:otherwise>
+ </xsl:choose>
+ </a>
+ <xsl:if test="not($body='NO')">
+ <xsl:text> </xsl:text>
+ <a href="" target="{$target}"
+ onClick="this.href=makeURL('{$target}','{concat($quoteduri,$quotedbodyname)}','{$ann}','{$types}')"
+ onMouseOver="window.status='{concat($quoteduri,$quotedname)}'; return true"
+ >Proof term</a>
+ </xsl:if>
+ <xsl:if test="not($proof_tree='NO')">
+ <xsl:text> </xsl:text>
+ <a href="" target="{$target}"
+ onClick="this.href=makeURL('{$target}','{concat($quoteduri,$quotedprooftreename)}','{$ann}','{$types}')"
+ onMouseOver="window.status='{concat($quoteduri,$quotedname)}'; return true"
+ >Proof tree</a>
+ </xsl:if>
</td>
</tr>
</xsl:template>