From 98bebe823e0b925f5b4bd3b0c70f1a966ae12758 Mon Sep 17 00:00:00 2001
From: Irene Schena <irene.schena@unibo.it>
Date: Thu, 22 Mar 2001 12:40:20 +0000
Subject: [PATCH] Modified Files: 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       |  1 +
 helm/style/mmltheoryextension.xsl | 42 +++++++++++++++++++++++++++++++
 helm/style/objcontent.xsl         | 20 ++++++---------
 helm/style/theory_pres.xsl        | 13 ++--------
 4 files changed, 52 insertions(+), 24 deletions(-)
 create mode 100644 helm/style/mmltheoryextension.xsl

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 6e66736a3..67859db65 100644
--- 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
index 000000000..d173c795d
--- /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 b9f77cb82..9b9825051 100644
--- 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 aa23acbe0..e2745fd06 100644
--- 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>
-
-
-
-
-
-
-
-
-
-- 
2.39.2