From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Jul 2004 14:05:21 +0000 (+0000)
Subject: cleanURI now removes also the part that follows the '#' symbol.
X-Git-Tag: pre_subst_in_kernel~3
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=13b68fb0980e89bd58536f1c56f89241ed1f6ac7;p=helm.git

cleanURI now removes also the part that follows the '#' symbol.
---

diff --git a/helm/on-line/xslt/resolve_topurl.xsl b/helm/on-line/xslt/resolve_topurl.xsl
index 695047108..c7f664374 100644
--- a/helm/on-line/xslt/resolve_topurl.xsl
+++ b/helm/on-line/xslt/resolve_topurl.xsl
@@ -103,17 +103,22 @@
 <xsl:template match="subst:cleanCICURI">
  <xsl:variable name="uri" select="$CICURI"/>
  <xsl:variable name="uri_before_body" select="substring-before($uri,'.body')"/>
- <xsl:variable name="cleanuri">
-  <xsl:choose>
-   <xsl:when test="$uri_before_body = ''">
-    <xsl:value-of select="$uri"/>
-   </xsl:when>
-   <xsl:otherwise>
-    <xsl:value-of select="$uri_before_body"/>
-   </xsl:otherwise>
-  </xsl:choose>
- </xsl:variable>
- <xsl:value-of select="$cleanuri"/>
+ <xsl:choose>
+  <xsl:when test="$uri_before_body = ''">
+   <xsl:variable name="uri_before_sharp" select="substring-before($uri,'#')"/>
+   <xsl:choose>
+    <xsl:when test="$uri_before_sharp = ''">
+     <xsl:value-of select="$uri"/>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:value-of select="$uri_before_sharp"/>
+    </xsl:otherwise>
+   </xsl:choose>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:value-of select="$uri_before_body"/>
+  </xsl:otherwise>
+ </xsl:choose>
 </xsl:template>
 
 <xsl:template match="subst:base_CICURI">