###############################################################

[helm.git] / helm / on-line / xslt / ls2html.xsl

diff --git a/helm/on-line/xslt/ls2html.xsl b/helm/on-line/xslt/ls2html.xsl
index 9302e5841b62a09b62d17013f4800e12a25386b2..80d6946e5e6e7e10407445929d633e2da94f7db8 100644 (file)
--- a/helm/on-line/xslt/ls2html.xsl
+++ b/helm/on-line/xslt/ls2html.xsl
@@ -10,9 +10,11 @@
 <!-- uri must end with '/' -->
 <xsl:param name="uri" select="''"/>
 <xsl:param name="keys" select="''"/>
+<xsl:param name="processorURL" select="''"/>
 <xsl:param name="getterURL" select="''"/>
 <xsl:param name="interfaceURL" select="''"/>
 <xsl:param name="target" select="''"/>
+<xsl:param name="profile" select="''"/>
 
 <xsl:template name="chop">
  <xsl:param name="uri" select="''"/>
@@ -55,12 +57,12 @@
        "top.{$target}uri='{$quoteduri}';
         refresh{$target}Header('{$interfaceURL}/html/library/header.html');
         var search='?keys={$keys}' +
+         '&amp;profile={$profile}' +
+        '&amp;param.profile={$profile}' +
          '&amp;xmluri=' + escape('{$getterURL}ls?format=xml'+'&amp;baseuri={$quoteduri}')+
          '&amp;param.uri={$quoteduri}' +
          '&amp;param.keys={$keys}' +
-         '&amp;param.getterURL={$getterURL}' +
-         '&amp;param.target={$target}' +
-         '&amp;param.interfaceURL={$interfaceURL}';
+         '&amp;param.target={$target}';
         var pathname = this.pathname;
         if (pathname.charAt(0) != '/')
          pathname = '/' + pathname;
@@ -148,7 +150,7 @@
    </xsl:variable>
    <xsl:value-of select="$name"/>
    <xsl:text> </xsl:text>
-   <a href="javascript: var _ = window.open(top.frames[0].makeURL('{$target}','{concat($quoteduri,$quotedname)}','{$ann}','{$types}'));"
+   <a href="javascript: var _ = window.open(top.frames[0].makeURL('{$target}','{concat($quoteduri,$quotedname)}','{$ann}','{$types}','{$profile}','{$processorURL}','{$interfaceURL}','{$getterURL}'));"
       onMouseOver="window.status='{concat($quoteduri,$quotedname)}'; return true"
    >
     <xsl:choose>
@@ -158,13 +160,13 @@
    </a>
    <xsl:if test="not($body='NO')">
     <xsl:text> </xsl:text>
-    <a href="javascript: var _ = window.open(top.frames[0].makeURL('{$target}','{concat($quoteduri,$quotedbodyname)}','{$ann}','{$types}'))"
+    <a href="javascript: var _ = window.open(top.frames[0].makeURL('{$target}','{concat($quoteduri,$quotedbodyname)}','{$ann}','{$types}','{$profile}','{$processorURL}','{$interfaceURL}','{$getterURL}'))"
        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="javascript: var _ = window.open(top.frames[0].makeURL('{$target}','{concat($quoteduri,$quotedprooftreename)}','{$ann}','{$types}'))"
+    <a href="javascript: var _ = window.open(top.frames[0].makeURL('{$target}','{concat($quoteduri,$quotedprooftreename)}','{$ann}','{$types}','{$profile}','{$processorURL}','{$interfaceURL}','{$getterURL}'))"
        onMouseOver="window.status='{concat($quoteduri,$quotedname)}'; return true"
     >Proof tree</a>
    </xsl:if>