Working only for HTML and MathML presentation.
Modified Files:
expandobj.xsl link.xsl links_library.xsl theory_content.xsl
theory_pres.xsl
<!-- First draft: March 08 2001, Irene Schena -->
<!--***********************************************************************-->
<!-- First draft: March 08 2001, Irene Schena -->
<!--***********************************************************************-->
-<xsl:stylesheet version="0.1" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+<xsl:stylesheet version="0.1" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:ht="http://www.cs.unibo.it/helm/namespaces/helm-theory">
<!--******************************************************************-->
<!-- Parameters containing the absolute path of the CIC file -->
<!--******************************************************************-->
<!-- Parameters containing the absolute path of the CIC file -->
<!-- THEORY CONTENT ELEMENTS -->
<!-- document cannot return HTML, transforming it into XML!!! -->
<!-- THEORY CONTENT ELEMENTS -->
<!-- document cannot return HTML, transforming it into XML!!! -->
-<xsl:template match="THEOREM|LEMMA|COROLLARY|FACT">
-<xsl:variable name="url"><xsl:call-template name="makeTheoryURL"><xsl:with-param name="type" select="1"/><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:variable>
+<xsl:template match="ht:THEOREM">
+<xsl:variable name="url"><xsl:call-template name="makeURL4embedding"><xsl:with-param name="type" select="1"/><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:variable>
<xsl:copy>
<xsl:copy-of select="@*"/>
<!--<xsl:variable name="doc" select="document(string($url))"/>
<xsl:copy>
<xsl:copy-of select="@*"/>
<!--<xsl:variable name="doc" select="document(string($url))"/>
</xsl:copy>
</xsl:template>
</xsl:copy>
</xsl:template>
-<xsl:template match="AXIOM|DEFINITION|VARIABLE">
-<xsl:param name="type" select="0"/><xsl:variable name="url"><xsl:call-template name="makeTheoryURL"><xsl:with-param name="type" select="0"/><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:variable>
+<xsl:template match="ht:AXIOM|ht:DEFINITION|ht:VARIABLE">
+<xsl:param name="type" select="0"/><xsl:variable name="url"><xsl:call-template name="makeURL4embedding"><xsl:with-param name="type" select="0"/><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:variable>
<xsl:copy>
<xsl:copy-of select="@*"/>
<xsl:copy-of select="document(string($url))"/>
<xsl:copy>
<xsl:copy-of select="@*"/>
<xsl:copy-of select="document(string($url))"/>
<!-- THEORY PRESENTATION ELEMENTS -->
<xsl:template match="ENTITY">
<!-- THEORY PRESENTATION ELEMENTS -->
<xsl:template match="ENTITY">
-<xsl:variable name="url"><xsl:call-template name="makeTheoryURL"><xsl:with-param name="type" select="@type"/><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:variable>
+<xsl:variable name="url"><xsl:call-template name="makeURL4embedding"><xsl:with-param name="type" select="@type"/><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:variable>
<xsl:copy-of select="document(string($url))"/>
</xsl:template>
<xsl:copy-of select="document(string($url))"/>
</xsl:template>
</xsl:copy>
</xsl:template>
</xsl:copy>
</xsl:template>
+</xsl:stylesheet>
\ No newline at end of file
</xsl:template>
<!-- _top to refresh the whole frameset (avoids the matrioska effect ;-) -->
</xsl:template>
<!-- _top to refresh the whole frameset (avoids the matrioska effect ;-) -->
-<xsl:template match="a[@href]">
+<!-- a[@href] doesn't match with every anchor elements!!! -->
+<xsl:template match="*[@href]">
<xsl:copy>
<xsl:copy-of select="@*"/>
<xsl:copy>
<xsl:copy-of select="@*"/>
- <xsl:attribute name="href">
- <xsl:call-template name="makeURL">
- <xsl:with-param name="uri" select="@href"/>
- </xsl:call-template>
- </xsl:attribute>
- <xsl:attribute name="target">cic</xsl:attribute>
+ <xsl:choose>
+ <xsl:when test="starts-with(@href,"cic")">
+ <xsl:attribute name="href">
+ <xsl:call-template name="makeURL">
+ <xsl:with-param name="uri" select="@href"/>
+ </xsl:call-template>
+ </xsl:attribute>
+ <xsl:attribute name="target">cic</xsl:attribute>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:attribute name="href">
+ <xsl:call-template name="makeTheoryURL">
+ <xsl:with-param name="uri" select="@href"/>
+ </xsl:call-template>
+ </xsl:attribute>
+ <xsl:attribute name="target">theory</xsl:attribute>
+ </xsl:otherwise>
+ </xsl:choose>
<xsl:apply-templates/>
</xsl:copy>
</xsl:template>
<xsl:apply-templates/>
</xsl:copy>
</xsl:template>
</xsl:template>
</xsl:stylesheet>
</xsl:template>
</xsl:stylesheet>
<xsl:variable name="quotedthkeys">
<xsl:call-template name="quote">
<xsl:variable name="quotedthkeys">
<xsl:call-template name="quote">
- <xsl:with-param name="s" select="$thkeys"/>
+ <xsl:with-param name="s" select="'T1,T2,L,E'"/>
</xsl:call-template>
</xsl:variable>
</xsl:call-template>
</xsl:variable>
-<xsl:variable name="quotedquotedthkeys">
+<xsl:variable name="quotedekeys">
<xsl:call-template name="quote">
<xsl:call-template name="quote">
- <xsl:with-param name="s" select="$quotedkeys"/>
+ <xsl:with-param name="s" select="$thkeys"/>
</xsl:call-template>
</xsl:variable>
</xsl:call-template>
</xsl:variable>
</xsl:call-template>
</xsl:variable>
</xsl:call-template>
</xsl:variable>
+<xsl:variable name="quotedquotedkeys">
+ <xsl:call-template name="quote">
+ <xsl:with-param name="s" select="$quotedkeys"/>
+ </xsl:call-template>
+</xsl:variable>
+
+<xsl:variable name="quotedquotedthkeys">
+ <xsl:call-template name="quote">
+ <xsl:with-param name="s" select="$quotedthkeys"/>
+ </xsl:call-template>
+</xsl:variable>
+
<xsl:variable name="header0"><xsl:value-of select="$interfaceURL"/>?url=</xsl:variable>
<xsl:variable name="header1"><xsl:value-of select="$escaped-processorURL"/>apply?keys=</xsl:variable>
<xsl:variable name="header2">&param.naturalLanguage=<xsl:value-of select="$naturalLanguage"/>&param.annotations=<xsl:value-of select="$annotations"/>&prop.media-type=<xsl:value-of select="$media-type"/>&param.media-type=<xsl:value-of select="$media-type"/>&prop.doctype-public=<xsl:value-of select="$escaped-doctype-public"/>&param.doctype-public=<xsl:value-of select="$escaped-doctype-public"/>&prop.encoding=<xsl:value-of select="$encoding"/>&param.encoding=<xsl:value-of select="$encoding"/>&param.keys=<xsl:value-of select="$quotedkeys"/>&param.getterURL=<xsl:value-of select="$escaped-getterURL"/>&param.processorURL=<xsl:value-of select="$escaped-processorURL"/>&param.interfaceURL=<xsl:value-of select="$escaped-interfaceURL"/>&xmluri=<xsl:value-of select="$absPath"/></xsl:variable>
<xsl:variable name="header0"><xsl:value-of select="$interfaceURL"/>?url=</xsl:variable>
<xsl:variable name="header1"><xsl:value-of select="$escaped-processorURL"/>apply?keys=</xsl:variable>
<xsl:variable name="header2">&param.naturalLanguage=<xsl:value-of select="$naturalLanguage"/>&param.annotations=<xsl:value-of select="$annotations"/>&prop.media-type=<xsl:value-of select="$media-type"/>&param.media-type=<xsl:value-of select="$media-type"/>&prop.doctype-public=<xsl:value-of select="$escaped-doctype-public"/>&param.doctype-public=<xsl:value-of select="$escaped-doctype-public"/>&prop.encoding=<xsl:value-of select="$encoding"/>&param.encoding=<xsl:value-of select="$encoding"/>&param.keys=<xsl:value-of select="$quotedkeys"/>&param.getterURL=<xsl:value-of select="$escaped-getterURL"/>&param.processorURL=<xsl:value-of select="$escaped-processorURL"/>&param.interfaceURL=<xsl:value-of select="$escaped-interfaceURL"/>&xmluri=<xsl:value-of select="$absPath"/></xsl:variable>
+<xsl:variable name="header3">&param.thkeys=<xsl:value-of select="$quotedekeys"/></xsl:variable>
<xsl:variable name="quotedheader1">
<xsl:call-template name="quote">
<xsl:variable name="quotedheader1">
<xsl:call-template name="quote">
</xsl:call-template>
</xsl:variable>
</xsl:call-template>
</xsl:variable>
+<xsl:variable name="quotedheader3">
+ <xsl:call-template name="quote">
+ <xsl:with-param name="s" select="$header3"/>
+ </xsl:call-template>
+</xsl:variable>
+
<!-- makeURL() maps URIs into URLs -->
<!-- The target of the URL is the whole frameset -->
<xsl:variable name="biquotedfixedheader">
<!-- makeURL() maps URIs into URLs -->
<!-- The target of the URL is the whole frameset -->
<xsl:variable name="biquotedfixedheader">
+ <xsl:value-of select="$header0"/>
+ <xsl:value-of select="$quotedheader1"/>
+ <xsl:value-of select="$quotedquotedkeys"/>
+ <xsl:value-of select="$quotedheader2"/>
+</xsl:variable>
+
+<xsl:variable name="biquotedthfixedheader">
<xsl:value-of select="$header0"/>
<xsl:value-of select="$quotedheader1"/>
<xsl:value-of select="$quotedquotedthkeys"/>
<xsl:value-of select="$header0"/>
<xsl:value-of select="$quotedheader1"/>
<xsl:value-of select="$quotedquotedthkeys"/>
<!-- type, instead, is not propagated -->
<xsl:template name="makeURL">
<xsl:param name="uri" select="''"/>
<!-- type, instead, is not propagated -->
<xsl:template name="makeURL">
<xsl:param name="uri" select="''"/>
- <xsl:value-of select="$biquotedfixedheader"/>
- <xsl:value-of select="$uri"/>%26param.CICURI%3D<xsl:value-of select="$uri"/>
+ <xsl:value-of select="$biquotedfixedheader"/>
+ <xsl:value-of select="$uri"/>%26param.CICURI%3D<xsl:value-of select="$uri"/>
+</xsl:template>
+<xsl:template name="makeTheoryURL">
+<xsl:param name="uri" select="''"/>
+ <xsl:value-of select="$biquotedthfixedheader"/>
+ <xsl:value-of select="$uri"/>%26param.CICURI%3D<xsl:value-of select="$uri"/>
+ <xsl:value-of select="$quotedheader3"/>
-<!-- makeTheoryURL() maps URIs into URLs -->
+<!-- makeURL4embedding() maps URIs into URLs -->
<!-- The target of the URL is only the processed document -->
<!-- The target of the URL is only the processed document -->
-<xsl:template name="makeTheoryURL">
+<xsl:template name="makeURL4embedding">
<xsl:param name="uri" select="''"/>
<xsl:param name="type" select="0"/>
<xsl:value-of select="$header1"/>
<xsl:param name="uri" select="''"/>
<xsl:param name="type" select="0"/>
<xsl:value-of select="$header1"/>
- <xsl:value-of select="$quotedthkeys"/>
+ <xsl:value-of select="$quotedekeys"/>
<xsl:value-of select="$header2"/>
<xsl:value-of select="$uri"/>&param.CICURI=<xsl:value-of select="$uri"/>&param.type=<xsl:value-of select="$type"/>
</xsl:template>
</xsl:stylesheet>
<xsl:value-of select="$header2"/>
<xsl:value-of select="$uri"/>&param.CICURI=<xsl:value-of select="$uri"/>&param.type=<xsl:value-of select="$type"/>
</xsl:template>
</xsl:stylesheet>
<!-- First draft: May 08 2000, Claudio Sacerdoti Coen, Irene Schena -->
<!--***********************************************************************-->
<!-- First draft: May 08 2000, Claudio Sacerdoti Coen, Irene Schena -->
<!--***********************************************************************-->
-<xsl:stylesheet version="0.1" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+<xsl:stylesheet version="0.1" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:ht="http://www.cs.unibo.it/helm/namespaces/helm-theory">
+<!-- THEORY and SUBTHEORIES -->
-<xsl:template match="Theory">
- <Theory name="{@uri}" uri="{@uri}">
- <xsl:apply-templates><xsl:with-param name="current_uri" select="string(@uri)"/></xsl:apply-templates>
- </Theory>
+<xsl:template match="ht:SECTION">
+<xsl:param name="current_uri" select="''"/>
+<xsl:param name="delim" select="''"/>
+ <ht:SECTION name="{@uri}">
+ <xsl:apply-templates><xsl:with-param name="current_uri" select="concat($current_uri,$delim,string(@uri))"/><xsl:with-param name="delim" select=""/""/></xsl:apply-templates>
+ </ht:SECTION>
-<xsl:template match="SECTION">
-<xsl:param name="current_uri"/>
- <SECTION>
- <xsl:apply-templates><xsl:with-param name="current_uri" select="concat($current_uri,"/",string(@uri))"/></xsl:apply-templates>
- </SECTION>
+<xsl:template match="ht:MUTUAL">
+<xsl:param name="current_uri" select="''"/>
+<xsl:param name="delim" select="''"/>
+ <ht:MUTUAL>
+ <xsl:apply-templates><xsl:with-param name="current_uri" select="$current_uri"/><xsl:with-param name="delim" select="$delim"/></xsl:apply-templates>
+ </ht:MUTUAL>
-<xsl:template match="THEOREM|LEMMA|COROLLARY|AXIOM|FACT|DEFINITION|
- VARIABLE">
-<xsl:param name="current_uri"/>
-<xsl:variable name="uri" select="concat(string($current_uri),"/",string(@uri))"/>
+<xsl:template match="ht:AXIOM|ht:DEFINITION|ht:THEOREM|ht:VARIABLE">
+<xsl:param name="current_uri" select="''"/>
+<xsl:param name="delim" select="''"/>
+<xsl:variable name="uri" select="concat(string($current_uri),$delim,string(@uri))"/>
+ <xsl:copy-of select="@as"/>
<xsl:attribute name="name"><xsl:value-of select="substring-before(@uri,".")"/></xsl:attribute>
<xsl:attribute name="uri"><xsl:value-of select="$uri"/></xsl:attribute>
</xsl:copy>
</xsl:template>
<xsl:attribute name="name"><xsl:value-of select="substring-before(@uri,".")"/></xsl:attribute>
<xsl:attribute name="uri"><xsl:value-of select="$uri"/></xsl:attribute>
</xsl:copy>
</xsl:template>
+<xsl:template match = "/|*">
+<xsl:param name="current_uri" select="''"/>
+<xsl:param name="delim" select="''"/>
+ <xsl:copy>
+ <xsl:copy-of select="@*"/>
+ <xsl:apply-templates><xsl:with-param name="current_uri" select="$current_uri"/><xsl:with-param name="delim" select="$delim"/></xsl:apply-templates>
+ </xsl:copy>
+</xsl:template>
+</xsl:stylesheet>
\ No newline at end of file
<!--***********************************************************************-->
<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
<!--***********************************************************************-->
<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
- xmlns:m="http://www.w3.org/1998/Math/MathML">
+ xmlns:ht="http://www.cs.unibo.it/helm/namespaces/helm-theory">
<!--<xsl:output method="html" encoding="iso-8859-1"/>-->
<xsl:output
<!--<xsl:output method="html" encoding="iso-8859-1"/>-->
<xsl:output
doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
doctype-system="DTD/xhtml1-transitional.dtd" />
doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
doctype-system="DTD/xhtml1-transitional.dtd" />
-<xsl:template match="Theory">
- <html>
- <head></head>
- <body>
- <h2>THEORY<xsl:text> </xsl:text><xsl:value-of select="@name"/></h2>
- <xsl:apply-templates select="*"/>
- <h2>END THEORY</h2>
- </body>
- </html>
+<xsl:template match="ht:SECTION">
+ <h3>BEGIN SECTION<xsl:text> </xsl:text><xsl:value-of select="@name"/></h3>
+ <xsl:apply-templates select="*"/>
+ <h3>END SECTION</h3>
-<xsl:template match="SECTION">
- <h3>BEGIN SECTION</h3>
+<xsl:template match="ht:MUTUAL">
+ <h4>BEGIN MUTUAL DEFINITIONS</h4>
<xsl:apply-templates select="*"/>
<xsl:apply-templates select="*"/>
+ <h4>END MUTUAL DEFINITIONS</h4>
-<xsl:template match="THEOREM|LEMMA|COROLLARY|FACT">
- <h4><xsl:value-of select="name(.)"/><xsl:text> </xsl:text><a href="{@uri}"><xsl:value-of select="@name"/></a></h4>
+<xsl:template match="ht:THEOREM">
+ <h5><xsl:value-of select="@as"/><xsl:text> </xsl:text><a href="{@uri}"><xsl:value-of select="@name"/></a></h5>
<ENTITY uri="{@uri}" type="1"/>
</xsl:template>
<ENTITY uri="{@uri}" type="1"/>
</xsl:template>
-<xsl:template match="AXIOM|DEFINITION|VARIABLE">
- <h4><xsl:value-of select="name(.)"/><xsl:text> </xsl:text><a href="{@uri}"><xsl:value-of select="@name"/></a></h4>
+<xsl:template match="ht:AXIOM|ht:VARIABLE">
+ <h5><xsl:value-of select="substring-after(string(name(.)), "ht:")"/><xsl:text> </xsl:text><a href="{@uri}"><xsl:value-of select="@name"/></a></h5>
+ <ENTITY uri="{@uri}" type="0"/>
+</xsl:template>
+
+<xsl:template match="ht:DEFINITION">
+<xsl:variable name="name"><xsl:choose><xsl:when test="@as='Inductive'">Inductive Definition</xsl:when><xsl:when test="@as='CoInductive'">CoInductive Definition</xsl:when><xsl:when test="@as='Record'">Record Definition</xsl:when><xsl:otherwise>Definition</xsl:otherwise></xsl:choose></xsl:variable>
+ <h5><xsl:value-of select="string($name)"/><xsl:text> </xsl:text><a href="{@uri}"><xsl:value-of select="@name"/></a></h5>
<ENTITY uri="{@uri}" type="0"/>
</xsl:template>
<ENTITY uri="{@uri}" type="0"/>
</xsl:template>
+<!-- Root and XHTML -->
+
+<xsl:template match = "/|*">
+ <xsl:copy>
+ <xsl:copy-of select="@*"/>
+ <xsl:apply-templates/>
+ </xsl:copy>
+</xsl:template>
+