From c2240adf58d6e77973bb057f09e2232852046bf8 Mon Sep 17 00:00:00 2001
From: Irene Schena <irene.schena@unibo.it>
Date: Mon, 19 Mar 2001 10:42:54 +0000
Subject: [PATCH] Modified Files: 1) expandobj.xsl, params.xsl,
 theory_content.xsl, theory_pres.xsl: new structurefor theories 2) params.xsl:
 adding mode="pure" in abstparams Added Files: 1) objtheorycontent.xsl: new
 content generation for objects in theories

---
 helm/style/expandobj.xsl        |  49 ++++++----
 helm/style/objtheorycontent.xsl | 165 ++++++++++++++++++++++++++++++++
 helm/style/params.xsl           |  13 ++-
 helm/style/theory_content.xsl   |  12 ++-
 helm/style/theory_pres.xsl      |  33 ++++---
 5 files changed, 232 insertions(+), 40 deletions(-)
 create mode 100644 helm/style/objtheorycontent.xsl

diff --git a/helm/style/expandobj.xsl b/helm/style/expandobj.xsl
index baf2007c7..ea313b758 100644
--- a/helm/style/expandobj.xsl
+++ b/helm/style/expandobj.xsl
@@ -36,14 +36,17 @@
 <!--******************************************************************-->
 <xsl:param name="getterURL" select="'http://localhost:8081/'"/>
 <xsl:param name="processorURL" select="'http://localhost:8080/helm/servlet/uwobo/'"/>
-<!-- Keys contains the keys of the stylesheets to be applied -->
+<!-- Keys contains the keys of the stylesheets to be applied following links-->
 <xsl:param name="keys" select="'C1,C2'"/>
+<!-- Thkeys contains the keys of the stylesheets to be applied at the first 
+step for expanding objects --> 
+<xsl:param name="thkeys" select="'TC1,C2'"/>
 <xsl:param name="naturalLanguage" select="'yes'"/>
 <xsl:param name="annotations" select="'no'"/>
 
 <xsl:variable name="absPath"><xsl:value-of select="$getterURL"/>getxml?uri=</xsl:variable>
 
-<xsl:variable name="header"><xsl:value-of select="$processorURL"/>apply?keys=<xsl:value-of select="$keys"/>&#x26;param.naturalLanguage=<xsl:value-of select="$naturalLanguage"/>&#x26;param.annotations=<xsl:value-of select="$annotations"/>&#x26;param.keys=<xsl:value-of select="$keys"/>&#x26;param.getterURL=<xsl:value-of select="$getterURL"/>&#x26;param.processorURL=<xsl:value-of select="$processorURL"/>&#x26;xmluri=<xsl:value-of select="$absPath"/></xsl:variable>
+<xsl:variable name="header"><xsl:value-of select="$processorURL"/>apply?keys=<xsl:value-of select="$thkeys"/>&#x26;param.naturalLanguage=<xsl:value-of select="$naturalLanguage"/>&#x26;param.annotations=<xsl:value-of select="$annotations"/>&#x26;param.keys=<xsl:value-of select="$keys"/>&#x26;param.getterURL=<xsl:value-of select="$getterURL"/>&#x26;param.processorURL=<xsl:value-of select="$processorURL"/>&#x26;xmluri=<xsl:value-of select="$absPath"/></xsl:variable>
 
 <xsl:output 
 	method="xml"
@@ -52,34 +55,44 @@
  	doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
   	doctype-system="DTD/xhtml1-transitional.dtd" />
 
-
 <!-- Generates an url from an uri -->
 <!-- DUPLICATO in content_to_html!! -->
 
 <xsl:template name="makeURL">
- <xsl:param name="uri" select="''"/>
- <xsl:value-of select="concat(string($header),string($uri),'&#x26;param.CICURI=',string($uri))"/>
+<xsl:param name="type" select="0"/>
+<xsl:param name="uri" select="''"/>
+  <xsl:value-of select="concat(string($header),string($uri),'&#x26;param.CICURI=',string($uri),'&#x26;param.type=',string($type))"/>
 </xsl:template>
 
-<!-- CONTENT THEORY AND SUBTHEORY -->
+<!-- THEORY CONTENT ELEMENTS -->
+<!-- document cannot return HTML, transforming it into XML!!! -->
 
-<xsl:template match="SECTION">
-    <SECTION>
-     <xsl:apply-templates/>
-    </SECTION>
+<xsl:template match="THEOREM|LEMMA|COROLLARY|FACT">
+<xsl:variable name="url"><xsl:call-template name="makeURL"><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:value-of select="$doc"/>-->
+    <xsl:copy-of select="document(string($url))"/>
+   </xsl:copy>
 </xsl:template>
 
-<!-- THEORY ELEMENTS -->
-<!-- document cannot return HTML, transforming it into XML!!! -->
+<xsl:template match="AXIOM|DEFINITION|VARIABLE">
+<xsl:variable name="url"><xsl:call-template name="makeURL"><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:template>
+
+<!-- THEORY PRESENTATION ELEMENTS -->
 
 <xsl:template match="ENTITY">
-<xsl:variable name="url"><xsl:call-template name="makeURL"><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:variable>
-<!--<xsl:variable name="doc" select="document(string($url))"/>
-<xsl:value-of select="$doc"/>-->
+<xsl:variable name="url"><xsl:call-template name="makeURL"><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>
 
-<!-- PRESENTATION THEORY AND SUBTHEORY -->
+<!-- CONTENT AND PRESENTATION THEORY AND SUBTHEORY -->
 
 <xsl:template match = "/|*">
   <xsl:copy>
@@ -92,7 +105,3 @@
 
 
 
-
-
-
-
diff --git a/helm/style/objtheorycontent.xsl b/helm/style/objtheorycontent.xsl
new file mode 100644
index 000000000..6b860a0a4
--- /dev/null
+++ b/helm/style/objtheorycontent.xsl
@@ -0,0 +1,165 @@
+<?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/.                                         -->
+
+<!--******************************************************************--> 
+<!-- XSLT version 0.1 of CIC objects to MathML content of types only: -->
+<!-- First draft: March 9 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:param name="type" select="0"/>
+<xsl:param name="getterURL" select="'http://localhost:8081/'"/>
+<xsl:variable name="absPath"><xsl:value-of select="$getterURL"/>getciconly?uri=</xsl:variable>
+
+<xsl:import href="objcontent.xsl"/>
+<xsl:include href="basic.xsl"/>
+<xsl:include href="set.xsl"/>
+<xsl:include href="reals.xsl"/>
+
+<!-- CIC DEFINITION -->
+
+<xsl:template match="Definition">
+    <xsl:choose>
+    <xsl:when test="$type=0">
+     <Definition name="{@name}" helm:xref="{@id}">  
+      <xsl:if test="string(@params) != &quot;&quot;">
+       <Params>
+        <xsl:value-of select="@params"/>
+       </Params>
+      </xsl:if>
+      <body>
+       <xsl:apply-templates select="body/*[1]"/>
+      </body>
+     <type>
+       <xsl:apply-templates select="type/*[1]"/>
+     </type>
+    </Definition>
+   </xsl:when>
+   <xsl:otherwise>
+    <type>
+     <xsl:apply-templates select="type/*[1]"/>
+    </type>
+   </xsl:otherwise>
+   </xsl:choose>
+</xsl:template>
+
+<xsl:template match="Axiom|CurrentProof|InductiveDefinition|Variable">
+    <xsl:apply-templates select="." mode="noannot"/>
+</xsl:template>
+
+<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX">
+    <m:math>
+     <xsl:apply-templates select="." mode="noannot"/>
+    </m:math>
+</xsl:template>
+
+<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX" mode="noannot">
+    <xsl:apply-templates select="." mode="pure"/>
+</xsl:template>
+
+</xsl:stylesheet>
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/helm/style/params.xsl b/helm/style/params.xsl
index b4d83bce8..eebda7e87 100644
--- a/helm/style/params.xsl
+++ b/helm/style/params.xsl
@@ -309,7 +309,8 @@
      <xsl:when test="($target = 1) and ($noparams != 0)">
       <m:apply>
       <m:csymbol>app</m:csymbol>
-      <xsl:apply-templates select="."/>
+<!-- Mancava modalita': sono qall'interno di un termine -->
+      <xsl:apply-templates select="." mode="pure"/>
       <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noparams"/></xsl:call-template>
       </m:apply>
      </xsl:when>
@@ -320,7 +321,15 @@
       </xsl:when>
       <xsl:otherwise>
        <xsl:if test="$target = 1">
-        <xsl:apply-templates select="."/>
+<!-- Mancava modalita': con target=1 posso provenire sia da un oggetto che da un termine -->
+        <xsl:choose>
+        <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
+         <xsl:apply-templates select="." mode="pure"/>
+        </xsl:when>
+        <xsl:otherwise>
+         <xsl:apply-templates select="."/>
+        </xsl:otherwise>
+        </xsl:choose>
        </xsl:if>
       </xsl:otherwise>
       </xsl:choose>
diff --git a/helm/style/theory_content.xsl b/helm/style/theory_content.xsl
index 6ae6ee7c9..4a7b4adc3 100644
--- a/helm/style/theory_content.xsl
+++ b/helm/style/theory_content.xsl
@@ -35,9 +35,9 @@
 <!-- THEORY -->
 
 <xsl:template match="Theory">
-    <SECTION>
+    <Theory name="{@uri}" uri="{@uri}">
      <xsl:apply-templates><xsl:with-param name="current_uri" select="string(@uri)"/></xsl:apply-templates>
-    </SECTION>
+    </Theory>
 </xsl:template>
 
 <!-- SUBTHEORY -->
@@ -51,10 +51,14 @@
 
 <!-- THEORY ELEMENTS -->
 
-<xsl:template match="DEFINITION|AXIOM|THEOREM|VARIABLE">
+<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))"/>
-    <ENTITY uri="{$uri}"/>
+    <xsl:copy>
+     <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>
diff --git a/helm/style/theory_pres.xsl b/helm/style/theory_pres.xsl
index 5d60b9efa..b4a6e3cd8 100644
--- a/helm/style/theory_pres.xsl
+++ b/helm/style/theory_pres.xsl
@@ -41,29 +41,31 @@
  	doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
   	doctype-system="DTD/xhtml1-transitional.dtd" />
 
-<xsl:template match="SECTION">
-<xsl:param name="subsect" select="0"/>
-    <xsl:choose>
-    <xsl:when test="$subsect = 0">
+<xsl:template match="Theory">
      <html> 
       <head></head>
       <body>
-       <h3>BEGIN SECTION</h3>
-       <xsl:apply-templates select="*"><xsl:with-param name="subsect" select="1"/></xsl:apply-templates>
-       <h3>END SECTION</h3>
+       <h2>THEORY<xsl:text>&#x00a0;</xsl:text><xsl:value-of select="@name"/></h2>
+       <xsl:apply-templates select="*"/>
+       <h2>END THEORY</h2>
       </body>
      </html>
-    </xsl:when>
-    <xsl:otherwise>
+</xsl:template>
+
+<xsl:template match="SECTION">
      <h3>BEGIN SECTION</h3>
-      <xsl:apply-templates select="*"><xsl:with-param name="subsect" select="1"/></xsl:apply-templates>
+     <xsl:apply-templates select="*"/>
      <h3>END SECTION</h3>
-    </xsl:otherwise>
-    </xsl:choose>
 </xsl:template>
 
-<xsl:template match="ENTITY">
-  <ENTITY uri="{@uri}"/>
+<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>
+    <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>
+    <ENTITY uri="{@uri}" type="0"/>
 </xsl:template>
 
 </xsl:stylesheet>
@@ -73,3 +75,6 @@
 
 
 
+
+
+
-- 
2.39.2