]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 98a2af5)
Modified Files:
authorIrene Schena <irene.schena@unibo.it>
Thu, 22 Mar 2001 12:40:20 +0000 (12:40 +0000)
committerIrene Schena <irene.schena@unibo.it>
Thu, 22 Mar 2001 12:40:20 +0000 (12:40 +0000)
1) mmlextension.xsl: added import of mmltheoryextension.xsl
2) objcontent.xsl: added *[1] to apply-templates
Added Files:
1) mmltheoryextension.xsl: MML presentation of objects in theories

helm/style/mmlextension.xsl patch | blob | history
helm/style/mmltheoryextension.xsl [new file with mode: 0644] patch | blob
helm/style/objcontent.xsl patch | blob | history
helm/style/theory_pres.xsl patch | blob | history

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 6e66736a32aeb8e1fc866033a8091fc511f028f7..67859db656d243d62babbc0a06ecc6dea80cf792 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -37,6 +37,7 @@
                               xmlns:helm="http://www.cs.unibo.it/helm">
 
 <xsl:import href="mml2mmlv1_0.xsl"/>
+<xsl:import href="mmltheoryextension.xsl"/>
 
 <!--***********************************************************************-->
 <!-- Parameter affecting line-breaking                                     -->
diff --git a/helm/style/mmltheoryextension.xsl b/helm/style/mmltheoryextension.xsl
new file mode 100644 (file)
index 0000000..d173c79
--- /dev/null
+++ b/helm/style/mmltheoryextension.xsl
@@ -0,0 +1,42 @@
+<?xml version="1.0"?>
+
+<!-- Copyright (C) 2000, HELM Team                                     -->
+<!--                                                                   -->
+<!-- This file is part of HELM, an Hypertextual, Electronic            -->
+<!-- Library of Mathematics, developed at the Computer Science         -->
+<!-- Department, University of Bologna, Italy.                         -->
+<!--                                                                   -->
+<!-- HELM is free software; you can redistribute it and/or             -->
+<!-- modify it under the terms of the GNU General Public License       -->
+<!-- as published by the Free Software Foundation; either version 2    -->
+<!-- of the License, or (at your option) any later version.            -->
+<!--                                                                   -->
+<!-- HELM is distributed in the hope that it will be useful,           -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
+<!-- GNU General Public License for more details.                      -->
+<!--                                                                   -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software               -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
+<!-- MA  02111-1307, USA.                                              -->
+<!--                                                                   -->
+<!-- For details, see the HELM World-Wide-Web page,                    -->
+<!-- http://cs.unibo.it/helm/.                                         -->
+
+<!--***********************************************************************--> 
+<!-- Extension to the XSLT version 0.07 of MathML content to presentation: -->
+<!-- First draft: March 22 2001, Irene Schena                              -->
+<!--***********************************************************************--> 
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:m="http://www.w3.org/1998/Math/MathML"
+                              xmlns:helm="http://www.cs.unibo.it/helm">
+
+<xsl:template match="type">
+    <m:math>
+     <xsl:apply-templates select="*[1]"/>
+    </m:math>
+</xsl:template>
+
+</xsl:stylesheet>
diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl
index b9f77cb82700afbf9cddabcb7b7669b59d3532a8..9b98250511fba36ef67907a29c777035ad1ab7ff 100644 (file)
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -74,10 +74,10 @@
       </xsl:otherwise>
      </xsl:choose> -->
      <body>
-      <xsl:apply-templates select="body/*"/>
+      <xsl:apply-templates select="body/*[1]"/>
      </body>
      <type>
-       <xsl:apply-templates select="type/*"/>
+       <xsl:apply-templates select="type/*[1]"/>
      </type>
     </Definition> 
 </xsl:template>
@@ -90,7 +90,7 @@
       </Params>
      </xsl:if>
      <type>
-       <xsl:apply-templates select="type/*"/>
+       <xsl:apply-templates select="type/*[1]"/>
      </type>
     </Axiom> 
 </xsl:template>
@@ -103,10 +103,10 @@
       </Conjecture>
      </xsl:for-each>
      <body>
-       <xsl:apply-templates select="body/*"/>
+       <xsl:apply-templates select="body/*[1]"/>
      </body>
      <type>
-       <xsl:apply-templates select="type/*"/>
+       <xsl:apply-templates select="type/*[1]"/>
      </type>
     </CurrentProof> 
 </xsl:template>
@@ -148,19 +148,13 @@
     <Variable name="{@name}" helm:xref="{@id}">
      <xsl:if test="name(*[1])='body'">
       <body>
-       <xsl:apply-templates select="body/*"/>
+       <xsl:apply-templates select="body/*[1]"/>
       </body>
      </xsl:if>
      <type>
-       <xsl:apply-templates select="type/*"/>
+       <xsl:apply-templates select="type/*[1]"/>
      </type>
     </Variable> 
 </xsl:template>
 
 </xsl:stylesheet>
-
-
-
-
-
-
diff --git a/helm/style/theory_pres.xsl b/helm/style/theory_pres.xsl
index aa23acbe0ed5b35cbdd6997d096181a29777533b..e2745fd0625c3c4a01734e16714bec1cd64d0aa7 100644 (file)
--- a/helm/style/theory_pres.xsl
+++ b/helm/style/theory_pres.xsl
@@ -59,22 +59,13 @@
 </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>
+    <h4><xsl:value-of select="name(.)"/><xsl:text>&#x00a0;</xsl:text><a href="{@uri}"><xsl:value-of select="@name"/></a></h4>
     <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>
+    <h4><xsl:value-of select="name(.)"/><xsl:text>&#x00a0;</xsl:text><a href="{@uri}"><xsl:value-of select="@name"/></a></h4>
     <ENTITY uri="{@uri}" type="0"/>
 </xsl:template>
 
 </xsl:stylesheet>
-
-
-
-
-
-
-
-
-
Unnamed repository; edit this file 'description' to name the repository.