From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 10 Apr 2003 17:04:01 +0000 (+0000)
Subject: @uri attribute added to tacticinstance. A "Tactic details" hyperlink is
X-Git-Tag: before_refactoring~25
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e9db2c226034b75e69dba72b6bd577a7bcf6a31f;p=helm.git

@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 d45eb8b00..5fb0c0d8a 100644
--- 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 343cafd63..8ba633db6 100644
--- 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>