<?xml version="1.0"?>
<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:helm="http://www.cs.unibo.it/helm"
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">
- <script language="{@language}" src="{concat($topurl,@src)}"></script>
+ <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:CICURL">
+ <xsl:call-template name="makeCICURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:HTMLURL">
+ <xsl:call-template name="makeHTMLURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:MathMLPresentationURL">
+ <xsl:call-template name="makeMathMLPresentationURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:MathMLContentURL">
+ <xsl:call-template name="makeMathMLContentURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:DirectRDFURL">
+ <xsl:call-template name="makeDirectRDFURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:InverseRDFURL">
+ <xsl:call-template name="makeInverseRDFURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:DCRDFURL">
+ <xsl:call-template name="makeDCRDFURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:CICURI">
+ <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: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:topurl">
- <xsl:value-of select="$topurl"/>
+<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:makeProofTreeURL">
+ <xsl:call-template name="makeProofTreeURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ <xsl:with-param name="createframeset" select="false()"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:makeHTMLURLwithProfile">
+ <xsl:call-template name="makeHTMLURLwithProfile">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ <xsl:with-param name="profile" select="@profile"/>
+ </xsl:call-template>
+</xsl:template>
+
+<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="subst:makeTheoryURLwithProfile">
+ <xsl:call-template name="makeTheoryURLwithProfile">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ <xsl:with-param name="createframeset" select="true()"/>
+ <xsl:with-param name="profile" select="@profile"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:makeDirectDependencyURL">
+ <xsl:call-template name="makeDirectDependenciesURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:makeRecDependencyURL">
+ <xsl:call-template name="makeGraphURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ <xsl:with-param name="keys" select="'MDG'"/>
+ <xsl:with-param name="uri_set_size" select="$uri_set_size"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:makeInverseDirectDependencyURL">
+ <xsl:call-template name="makeInverseDirectDependenciesURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:makeInverseRecDependencyURL">
+ <xsl:call-template name="makeGraphURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ <xsl:with-param name="keys" select="'MMG'"/>
+ <xsl:with-param name="uri_set_size" select="$uri_set_size"/>
+ </xsl:call-template>
+</xsl:template>
+
+<!-- used by moogle -->
+
+<xsl:template match="helm:uwobo_form">
+ <form action="{concat($processorURL,'apply?')}" method="get">
+ <xsl:apply-templates select="*"/>
+ </form>
+</xsl:template>
+
+<xsl:template match = "helm:hidden_params">
+ <xsl:call-template name="hidden_params"/>
+</xsl:template>
+
+<xsl:template match = "helm:j_params">
+ <xsl:call-template name="j_params"/>
+</xsl:template>
+
+<xsl:template name="hidden_params">
+ <input type="hidden" name="xmluri" value="{concat($getterURL,'getempty')}"/>
+ <input type="hidden" name="param.profile" value="{$profile}"/>
+ <input type="hidden" name="profile" value="{$profile}"/>
+ <input type="hidden" name="param.keys" value="{$keys}"/>
+ <input type="hidden" name="param.embedkeys" value="{$embedkeys}"/>
+ <input type="hidden" name="param.thkeys" value="{$thkeys}"/>
+ <input type="hidden" name="param.prooftreekeys" value="{$prooftreekeys}"/>
+
+ <input type="hidden" name="param.media-type" value="{$media-type}"/>
+ <input type="hidden" name="param.thmedia-type" select="{$thmedia-type}"/>
+ <input type="hidden" name="prooftreemedia-type" select="{$prooftreemedia-type}"/>
+ <input type="hidden" name="param.doctype-public" select="{$doctype-public}"/>
+ <input type="hidden" name="param.encoding" select="{$encoding}"/>
+ <input type="hidden" name="param.thencoding" select="{$thencoding}"/>
+ <input type="hidden" name="param.prooftreeencoding" select="{$prooftreeencoding}"/>
+</xsl:template>
+
+<xsl:template name="j_params">
+ <input type="hidden" name="j_xmluri" value="{concat($getterURL,'getempty')}"/>
+ <input type="hidden" name="j_processorURL" value="{$processorURL}"/>
+ <input type="hidden" name="j_profile" value="{$profile}"/>
+ <input type="hidden" name="j_keys" value="{$keys}"/>
+ <input type="hidden" name="j_embedkeys" value="{$embedkeys}"/>
+ <input type="hidden" name="j_thkeys" value="{$thkeys}"/>
+ <input type="hidden" name="j_prooftreekeys" value="{$prooftreekeys}"/>
+
+ <input type="hidden" name="j_media_type" value="{$media-type}"/>
+ <input type="hidden" name="j_thmedia_type" select="{$thmedia-type}"/>
+ <input type="hidden" name="j_prooftreemedia_type" select="{$prooftreemedia-type}"/>
+ <input type="hidden" name="j_doctype_public" select="{$doctype-public}"/>
+ <input type="hidden" name="j_encoding" select="{$encoding}"/>
+ <input type="hidden" name="j_thencoding" select="{$thencoding}"/>
+ <input type="hidden" name="j_prooftreeencoding" select="{$prooftreeencoding}"/>
</xsl:template>
<xsl:template match="/|*">
projects / helm.git / blobdiff