Theory level DTD changed and .theory.xml files exported again.

Working only for HTML and MathML presentation.

Modified Files:
expandobj.xsl link.xsl links_library.xsl theory_content.xsl
theory_pres.xsl

diff --git a/helm/style/expandobj.xsl b/helm/style/expandobj.xsl
index a16176be5c05c2a44dbfe298a6925263ce9c280f..5a7b74ea2ff1935e7170668b8038cf71d020859a 100644 (file)
--- a/helm/style/expandobj.xsl
+++ b/helm/style/expandobj.xsl
@@ -29,7 +29,8 @@
 <!-- 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          -->
@@ -47,8 +48,8 @@
 <!-- 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))"/>
@@ -57,8 +58,8 @@
    </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))"/>
@@ -68,7 +69,7 @@
 <!-- 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>
 
@@ -81,4 +82,4 @@
   </xsl:copy>
 </xsl:template>
 
-</xsl:stylesheet>
+</xsl:stylesheet>
\ No newline at end of file

diff --git a/helm/style/link.xsl b/helm/style/link.xsl
index d5af006e1d72e3b2dc5ada821b1639d0c9fb5964..d3c78eaff1522182fe734206fd826ee6e3c09340 100644 (file)
--- a/helm/style/link.xsl
+++ b/helm/style/link.xsl
@@ -55,15 +55,28 @@
 </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: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,&quot;cic&quot;)">
+     <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>
@@ -76,3 +89,4 @@
 </xsl:template>
 
 </xsl:stylesheet> 
+

diff --git a/helm/style/links_library.xsl b/helm/style/links_library.xsl
index 7befa7bac8ec33218a8966e561e40e458e908938..a3000f3e8ef65dc0ccaa81e7e82cd7976dd45b2f 100644 (file)
--- a/helm/style/links_library.xsl
+++ b/helm/style/links_library.xsl
@@ -133,13 +133,13 @@ step for expanding objects -->
 
 <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:variable name="quotedquotedthkeys">
+<xsl:variable name="quotedekeys">
  <xsl:call-template name="quote">
-  <xsl:with-param name="s" select="$quotedkeys"/>
+  <xsl:with-param name="s" select="$thkeys"/>
  </xsl:call-template>
 </xsl:variable>
 
@@ -149,9 +149,22 @@ step for expanding objects -->
  </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">&#x26;param.naturalLanguage=<xsl:value-of select="$naturalLanguage"/>&#x26;param.annotations=<xsl:value-of select="$annotations"/>&#x26;prop.media-type=<xsl:value-of select="$media-type"/>&#x26;param.media-type=<xsl:value-of select="$media-type"/>&#x26;prop.doctype-public=<xsl:value-of select="$escaped-doctype-public"/>&#x26;param.doctype-public=<xsl:value-of select="$escaped-doctype-public"/>&#x26;prop.encoding=<xsl:value-of select="$encoding"/>&#x26;param.encoding=<xsl:value-of select="$encoding"/>&#x26;param.keys=<xsl:value-of select="$quotedkeys"/>&#x26;param.getterURL=<xsl:value-of select="$escaped-getterURL"/>&#x26;param.processorURL=<xsl:value-of select="$escaped-processorURL"/>&#x26;param.interfaceURL=<xsl:value-of select="$escaped-interfaceURL"/>&#x26;xmluri=<xsl:value-of select="$absPath"/></xsl:variable>
+<xsl:variable name="header3">&#x26;param.thkeys=<xsl:value-of select="$quotedekeys"/></xsl:variable>
 
 <xsl:variable name="quotedheader1">
  <xsl:call-template name="quote">
@@ -165,10 +178,23 @@ step for expanding objects -->
  </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">
+ <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"/>
@@ -180,20 +206,29 @@ step for expanding objects -->
 <!-- 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"/>
 </xsl:template>
 
-<!-- makeTheoryURL() maps URIs into URLs                  -->
+<!-- makeURL4embedding() maps URIs into URLs              -->
 <!-- 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:value-of select="$quotedthkeys"/>
+ <xsl:value-of select="$quotedekeys"/>
  <xsl:value-of select="$header2"/>
  <xsl:value-of select="$uri"/>&#x26;param.CICURI=<xsl:value-of select="$uri"/>&#x26;param.type=<xsl:value-of select="$type"/>
 </xsl:template>
 
 </xsl:stylesheet> 
+
+
+

diff --git a/helm/style/theory_content.xsl b/helm/style/theory_content.xsl
index 4a7b4adc3f8fb9bf6778baa9424dbdace3e681ab..507370edb2f2e09678bb5ebafdca6fdf83fb0fed 100644 (file)
--- a/helm/style/theory_content.xsl
+++ b/helm/style/theory_content.xsl
@@ -29,41 +29,53 @@
 <!-- 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 -->
+<!-- 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="&quot;/&quot;"/></xsl:apply-templates>
+    </ht:SECTION>
 </xsl:template>
 
-<!-- SUBTHEORY -->
+<!-- MUTUAL -->
 
-<xsl:template match="SECTION">
-<xsl:param name="current_uri"/>
-    <SECTION>
-     <xsl:apply-templates><xsl:with-param name="current_uri" select="concat($current_uri,&quot;/&quot;,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>
 
+
 <!-- THEORY ELEMENTS -->
 
-<xsl:template match="THEOREM|LEMMA|COROLLARY|AXIOM|FACT|DEFINITION|
-                           VARIABLE">
-<xsl:param name="current_uri"/>
-<xsl:variable name="uri" select="concat(string($current_uri),&quot;/&quot;,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>
+     <xsl:copy-of select="@as"/>
      <xsl:attribute name="name"><xsl:value-of select="substring-before(@uri,&quot;.&quot;)"/></xsl:attribute>
      <xsl:attribute name="uri"><xsl:value-of select="$uri"/></xsl:attribute>
     </xsl:copy>
 </xsl:template>
 
-</xsl:stylesheet>
-
-
-
+<!-- Root and XHTML -->
 
+<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

diff --git a/helm/style/theory_pres.xsl b/helm/style/theory_pres.xsl
index e2745fd0625c3c4a01734e16714bec1cd64d0aa7..6456301a658be30be94664494b7341d5f110f709 100644 (file)
--- a/helm/style/theory_pres.xsl
+++ b/helm/style/theory_pres.xsl
@@ -31,7 +31,7 @@
 <!--***********************************************************************--> 
 
 <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 
@@ -41,31 +41,48 @@
        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>&#x00a0;</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>&#x00a0;</xsl:text><xsl:value-of select="@name"/></h3>
+     <xsl:apply-templates select="*"/>
+     <h3>END SECTION</h3>
 </xsl:template>
 
-<xsl:template match="SECTION">
-     <h3>BEGIN SECTION</h3>
+<xsl:template match="ht:MUTUAL">
+     <h4>BEGIN MUTUAL DEFINITIONS</h4>
      <xsl:apply-templates select="*"/>
-     <h3>END SECTION</h3>
+     <h4>END MUTUAL DEFINITIONS</h4>
 </xsl:template>
 
-<xsl:template match="THEOREM|LEMMA|COROLLARY|FACT">
-    <h4><xsl:value-of select="name(.)"/><xsl:text>&#x00a0;</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>&#x00a0;</xsl:text><a href="{@uri}"><xsl:value-of select="@name"/></a></h5>
     <ENTITY uri="{@uri}" type="1"/>
 </xsl:template>
 
-<xsl:template match="AXIOM|DEFINITION|VARIABLE">
-    <h4><xsl:value-of select="name(.)"/><xsl:text>&#x00a0;</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(.)), &quot;ht:&quot;)"/><xsl:text>&#x00a0;</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>&#x00a0;</xsl:text><a href="{@uri}"><xsl:value-of select="@name"/></a></h5>
     <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>
+
 </xsl:stylesheet>
+
+
+
+
+
+
+