@uri attribute added to tacticinstance. A "Tactic details" hyperlink is

now automatically generated starting from it.

diff --git a/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl b/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
index d45eb8b0019aa22095ba2cab137ce9a857c73394..5fb0c0d8aaec85dd4059d28f78543bfac4629bdb 100644 (file)
--- a/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
+++ b/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
@@ -34,7 +34,7 @@
 
 <xsl:param name="CICURI" select="''"/>
 <xsl:param name="type" select="'standalone'"/>
-<xsl:variable name="PIPPOUNICODEvsSYMBOL" select="'symbol'"/>
+<xsl:param name="UNICODEvsSYMBOL" select="'symbol'"/>
 <xsl:param name="explode_tactics" select="false()"/>
 
 <xsl:include href="nuprl_html_arith.xsl"/>
@@ -73,96 +73,96 @@
 <!--forall-->
   <xsl:variable name="forall">
     <xsl:choose>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">&quot;</xsl:when>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">&#x2200;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&quot;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x2200;</xsl:when>
       <xsl:otherwise>???</xsl:otherwise>
     </xsl:choose>
   </xsl:variable>
 <!--lambda-->
   <xsl:variable name="lambda">
     <xsl:choose>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">l</xsl:when>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">&#x3BB;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">l</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x3BB;</xsl:when>
       <xsl:otherwise>???</xsl:otherwise>
     </xsl:choose>
   </xsl:variable>
 <!--prod-->
   <xsl:variable name="prod">
     <xsl:choose>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">&#xD5;</xsl:when>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">&#x3A0;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xD5;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x3A0;</xsl:when>
       <xsl:otherwise>???</xsl:otherwise>
     </xsl:choose>
   </xsl:variable>
 <!--arrow-->
   <xsl:variable name="arrow">
     <xsl:choose>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">&#xAE;</xsl:when>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">&#x2192;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xAE;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x2192;</xsl:when>
       <xsl:otherwise>???</xsl:otherwise>
     </xsl:choose>
   </xsl:variable>
 <!--RightArrow-->
   <xsl:variable name="RightArrow">
     <xsl:choose>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">&#xDE;</xsl:when>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">&#x21D2;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xDE;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x21D2;</xsl:when>
       <xsl:otherwise>???</xsl:otherwise>
     </xsl:choose>
   </xsl:variable>
 <!--product-->
   <xsl:variable name="product">
     <xsl:choose>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">S</xsl:when>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">&#931;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">S</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#931;</xsl:when>
       <xsl:otherwise>???</xsl:otherwise>
     </xsl:choose>
   </xsl:variable>
 <!--member-->
   <xsl:variable name="member">
     <xsl:choose>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">&#xce;</xsl:when>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">&#8712;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xce;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#8712;</xsl:when>
       <xsl:otherwise>???</xsl:otherwise>
     </xsl:choose>
   </xsl:variable>
 <!--member-->
   <xsl:variable name="intersection">
     <xsl:choose>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">&#xc7;</xsl:when>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">&#8745;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xc7;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#8745;</xsl:when>
       <xsl:otherwise>???</xsl:otherwise>
     </xsl:choose>
   </xsl:variable>
 <!--integers-->
   <xsl:variable name="integers">
     <xsl:choose>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">I</xsl:when>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">&#921;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">I</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#921;</xsl:when>
       <xsl:otherwise>???</xsl:otherwise>
     </xsl:choose>
   </xsl:variable>
 <!--naturalnumbers-->
   <xsl:variable name="naturalnumbers">
     <xsl:choose>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">N</xsl:when>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">&#925;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">N</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#925;</xsl:when>
       <xsl:otherwise>???</xsl:otherwise>
     </xsl:choose>
   </xsl:variable>
 <!--implies-->
   <xsl:variable name="implies">
     <xsl:choose>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">&#xee;</xsl:when>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">&#8658;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xee;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#8658;</xsl:when>
       <xsl:otherwise>???</xsl:otherwise>
     </xsl:choose>
   </xsl:variable>
 <!--exists-->
   <xsl:variable name="exists">
     <xsl:choose>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">&#x24;</xsl:when>
-      <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">&#8707;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#x24;</xsl:when>
+      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#8707;</xsl:when>
       <xsl:otherwise>???</xsl:otherwise>
     </xsl:choose>
   </xsl:variable>
@@ -175,7 +175,7 @@
         <xsl:param name="size"   select="''"/>
 
         <xsl:choose>
-                <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">
+                <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
                         <FONT FACE="symbol" SIZE="{$size}" COLOR="{$color}">
                                 <xsl:value-of select="$symbol"/>
                         </FONT>
@@ -2789,6 +2789,7 @@
           <xsl:for-each select="TacticInstance/extra_info">
            <xsl:copy-of select="*|text()"/>
           </xsl:for-each>
+          <a style="text-decoration:underline ; color:green" href="{TacticInstance/@uri}">Tactic Details</a>
           <xsl:if test="$explode_tactics">
           <span ID="{$freshid4}">
             <a style="text-decoration:underline ; color:green" href="" onClick="Hide(document.getElementById('{$freshid4}'));Show(document.getElementById('{$freshid5}'));return (0==1);">Details</a>

diff --git a/helm/nuprl_stylesheets/nuprl_proof.xsl b/helm/nuprl_stylesheets/nuprl_proof.xsl
index 343cafd637e42a64880cd33cd7e550422e3e4397..8ba633db6c378b8fc16beb735a3f49dbdbc3474b 100644 (file)
--- a/helm/nuprl_stylesheets/nuprl_proof.xsl
+++ b/helm/nuprl_stylesheets/nuprl_proof.xsl
@@ -54,7 +54,7 @@
 </xsl:template>
 
 <xsl:template match="tacticinstance">
-  <TacticInstance name="{@name}">
+  <TacticInstance name="{@name}" uri="{@uri}">
     <xsl:apply-templates select="extra_info"/>
   </TacticInstance>
 </xsl:template>