From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 28 May 2004 14:12:21 +0000 (+0000)
Subject: Links in the control frame when the URI ends with .body are now handled
X-Git-Tag: pre_subst_in_kernel~51
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3d0a8583b20b11e0d184664fb667c3d17da17125;p=helm.git

Links in the control frame when the URI ends with .body are now handled
correctly (i.e. the .body is removed if meaningless, as for the proof-checker
or the metadata).
---

diff --git a/helm/on-line/html/cic/control.html b/helm/on-line/html/cic/control.html
index f41168d28..126772343 100644
--- a/helm/on-line/html/cic/control.html
+++ b/helm/on-line/html/cic/control.html
@@ -18,6 +18,7 @@ h2.uri { margin-top: 0ex; margin-bottom: 0ex }
 <script>
  var annotations="<subst:annotations/>";
  var CICURI="<subst:CICURI/>";
+ var cleanCICURI="<subst:cleanCICURI/>";
  var CICURL = "<subst:CICURL/>";
  var DCRDFURL = "<subst:DCRDFURL/>";
  var DirectRDFURL = "<subst:DirectRDFURL/>";
@@ -88,9 +89,9 @@ h2.uri { margin-top: 0ex; margin-bottom: 0ex }
   <li>
     <script>
      var url = processorURL + "apply?keys=MC%2CRT%2CL&amp;xmluri=" +
-         getterURL + "getxml%3Furi%3D" + CICURI +
+         getterURL + "getxml%3Furi%3D" + cleanCICURI +
          "&amp;prop.media-type=text/html&amp;prop.encoding=iso-8859-1" +
-         "&amp;param.CICURI=" + CICURI + "&amp;param.profile=" + profile +
+         "&amp;param.CICURI=" + cleanCICURI + "&amp;param.profile=" + profile +
          "&amp;profile=" + profile;
      document.write(
       '<a target="result" href="' + url + '">View metadata</a>'
@@ -99,7 +100,7 @@ h2.uri { margin-top: 0ex; margin-bottom: 0ex }
   </li>
   <li>
     <script>
-     url = proofcheckerURL + "proofCheck?uri=" + CICURI;
+     url = proofcheckerURL + "proofCheck?uri=" + cleanCICURI;
      document.write(
       '<a target="result" href="' + url + '">Proof check</a>'
      );
diff --git a/helm/on-line/xslt/resolve_topurl.xsl b/helm/on-line/xslt/resolve_topurl.xsl
index c2ad9e28c..a075e6a15 100644
--- a/helm/on-line/xslt/resolve_topurl.xsl
+++ b/helm/on-line/xslt/resolve_topurl.xsl
@@ -99,6 +99,22 @@
  <xsl:value-of select="$CICURI"/>
 </xsl:template>
 
+<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:template>
+
 <xsl:template match="subst:base_CICURI">
   <xsl:variable name="len" select="string-length($CICURI)" />
   <xsl:variable name="extension">