X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fnuprl_stylesheets%2Fnuprl_content_to_html2.xsl;h=ef15f1961ab592f13a804062a9e9a558cba2f7ea;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d45eb8b0019aa22095ba2cab137ce9a857c73394;hpb=734a6fc5d8da4896c646d1dd7a17afaf0dd33224;p=helm.git

diff --git a/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl b/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
index d45eb8b00..ef15f1961 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:variable name="NUPRLexists">
     <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>
@@ -2314,7 +2314,7 @@
 
 <xsl:template mode="inline" match="m:apply[m:exists]">
                <xsl:call-template name="mksymbol">
-		<xsl:with-param name="symbol" select="$exists"/>
+		<xsl:with-param name="symbol" select="$NUPRLexists"/>
         	<xsl:with-param name="color" select="'blue'"/>
 		<xsl:with-param name="size" select="'+0'"/>
 	</xsl:call-template>
@@ -2476,7 +2476,7 @@
 	<xsl:choose>
 	<xsl:when test="$charlength > $framewidth">
 	<xsl:call-template name="mksymbol">
-		<xsl:with-param name="symbol" select="$exists"/>
+		<xsl:with-param name="symbol" select="$NUPRLexists"/>
         	<xsl:with-param name="color" select="'blue'"/>
 		<xsl:with-param name="size" select="'+0'"/>
 	</xsl:call-template>
@@ -2785,10 +2785,7 @@
           </xsl:call-template>
           <xsl:text>By </xsl:text>
           <xsl:apply-templates select="TacticInstance/@name"/>
-          <!-- CSC: extra_info in HTML to be rendered here -->
-          <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>
@@ -2847,6 +2844,14 @@
 	  </xsl:if>
 </xsl:template>
 
+<!-- NuPRLDefinition -->
+
+<xsl:template match="NuPrlDefinition">
+ <xsl:apply-templates select="*[1]"/>
+ <xsl:text> := </xsl:text>
+ <xsl:apply-templates select="*[2]"/>
+</xsl:template>
+
 <!-- DEFINITION -->
 
 <xsl:template match="Definition">