]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/on-line/xslt/resolve_topurl.xsl
###############################################################
[helm.git] / helm / on-line / xslt / resolve_topurl.xsl
index 6cfe0eda0417efbb802da2454d876cecc0d17728..50fd991fc14845bbb8fad0c64d6f953de9614fad 100644 (file)
 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
                               xmlns:subst="http://www.cs.unibo.it/helm/subst">
 
+<xsl:import href="links_library.xsl"/>
+<xsl:import href="params.xsl"/>
+
 <xsl:output
            method="html" 
            encoding="ISO-8859-1" 
            media-type="text/html" />
 
-<xsl:param name="topurl" select="''"/>
+<xsl:param name="proofcheckerURL" select="''"/>
+<xsl:param name="interfaceURL" select="''"/>
+<xsl:param name="processorURL" select="''"/>
+<xsl:param name="getterURL" select="''"/>
+<xsl:param name="draw_graphURL" select="''"/>
+<xsl:param name="profile" select="''"/>
+<xsl:param name="url" select="''"/>
+<xsl:param name="CICURI" select="''"/>
+<xsl:param name="annotations" select="''"/>
 
 <xsl:template match="subst:script">
- <xsl:copy-of select="document(concat($topurl,@src,'_xml'))" />
+ <xsl:copy-of select="document(concat($interfaceURL,@src,'_xml'))" />
+</xsl:template>
+
+<xsl:template match="subst:proofcheckerURL">
+ <xsl:value-of select="$proofcheckerURL"/>
+</xsl:template>
+
+<xsl:template match="subst:interfaceURL">
+ <xsl:value-of select="$interfaceURL"/>
+</xsl:template>
+
+<xsl:template match="subst:processorURL">
+ <xsl:value-of select="$processorURL"/>
+</xsl:template>
+
+<xsl:template match="subst:getterURL">
+ <xsl:value-of select="$getterURL"/>
+</xsl:template>
+
+<xsl:template match="subst:draw_graphURL">
+ <xsl:value-of select="$draw_graphURL"/>
+</xsl:template>
+
+<xsl:template match="subst:profile">
+ <xsl:value-of select="$profile"/>
+</xsl:template>
+
+<xsl:template match="subst:url">
+ <xsl:value-of select="$url"/>
+</xsl:template>
+
+<xsl:template match="subst:CICURI">
+ <xsl:value-of select="$CICURI"/>
+</xsl:template>
+
+<xsl:template match="subst:base_CICURI">
+  <xsl:variable name="len" select="string-length($CICURI)" />
+  <xsl:variable name="extension">
+    <xsl:choose>
+      <xsl:when test="substring($CICURI,$len)='/'">#</xsl:when>
+      <xsl:when test="substring($CICURI,$len - 6)='.theory'">.theory</xsl:when>
+      <xsl:when test="substring($CICURI,$len - 3)='.con'">.con</xsl:when>
+      <xsl:when test="substring($CICURI,$len - 3)='.ind'">.ind</xsl:when>
+      <xsl:when test="substring($CICURI,$len - 3)='.var'">.var</xsl:when>
+      <xsl:when test="substring($CICURI,$len - 8)='.con.body'">.con.body</xsl:when>
+      <xsl:otherwise>
+<!--
+       <xsl:message terminate="no">
+         resolve_topurl.xsl: assertion failed
+       </xsl:message>
+-->
+      </xsl:otherwise>
+    </xsl:choose>
+  </xsl:variable>
+  <xsl:call-template name="name_of_uri">
+    <xsl:with-param name="uri">
+      <xsl:choose>
+       <xsl:when test="substring($CICURI,$len)='/'">
+         <xsl:value-of select="concat(substring($CICURI,1,$len - 1),'#')" />
+       </xsl:when>
+       <xsl:otherwise>
+         <xsl:value-of select="$CICURI" />
+       </xsl:otherwise>
+      </xsl:choose>
+    </xsl:with-param>
+    <xsl:with-param name="extension" select="$extension" />
+  </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:annotations">
+ <xsl:value-of select="$annotations"/>
+</xsl:template>
+
+<xsl:template match="subst:makeURL">
+ <xsl:call-template name="makeURL">
+  <xsl:with-param name="uri" select="$CICURI"/>
+  <xsl:with-param name="createframeset" select="false()"/>
+ </xsl:call-template>
 </xsl:template>
 
-<xsl:template match="subst:topurl">
- <xsl:value-of select="$topurl"/>
+<xsl:template match="subst:makeTheoryURL">
+ <xsl:call-template name="makeTheoryURL">
+  <xsl:with-param name="uri" select="$CICURI"/>
+  <xsl:with-param name="createframeset" select="false()"/>
+ </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="/|*">