* getter.xsl added

  In this stylesheet there is a simple function to make the URL
  of an XML file given its URI. (The URL is used to ask the getter
  to retrieve the file)
* every other stylesheet (but ricerca.xsl that is unused and
  links_library.xsl) has been changed to use the new function
  instead of computing the URL cutting&pasting the same code
  again and again.

diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index 2ce29b43ad68cf7f4299d7c44d87273a70c1625f..95a1f66b23a0d8bbb8a912f3f97e79d9b958c5d3 100644 (file)
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -182,51 +182,54 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
             </xsl:call-template>
          </xsl:with-param>
       </xsl:call-template>
- <!-- <xsl:value-of select="document(concat(string($absPath),@uri))/*/@name"/> -->
    </m:ci>
 </xsl:template>
 
 <xsl:template match="MUTIND" mode="pure">
     <m:ci definitionURL="{@uri}" helm:xref="{@id}">
+     <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:variable>
      <xsl:variable name="index"><xsl:value-of select="@noType"/></xsl:variable>
-     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="document(concat(string($absPath),@uri))/InductiveDefinition/InductiveType[position()=number($index)+1]/@name"/></xsl:with-param></xsl:call-template>
+     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="document($InductiveTypeUrl)/InductiveDefinition/InductiveType[position()=number($index)+1]/@name"/></xsl:with-param></xsl:call-template>
     </m:ci>
 </xsl:template>
 
 <xsl:template match="MUTCONSTRUCT" mode="pure">
     <m:ci definitionURL="{@uri}" helm:xref="{@id}">
+     <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:variable>
      <xsl:variable name="Tindex"><xsl:value-of select="@noType"/></xsl:variable>
      <xsl:variable name="Cindex"><xsl:value-of select="@noConstr"/></xsl:variable>
-     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="document(concat(string($absPath),@uri))/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($Cindex)]/@name"/></xsl:with-param></xsl:call-template>
+     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="document($InductiveTypeUrl)/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($Cindex)]/@name"/></xsl:with-param></xsl:call-template>
     </m:ci>
 </xsl:template>
 
 <xsl:template match="MUTCASE" mode="pure">
     <xsl:variable name="Tindex"><xsl:value-of select="@noType"/></xsl:variable>
     <xsl:variable name="Turi"><xsl:value-of select="@uriType"/></xsl:variable>
+     <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$Turi"/></xsl:call-template></xsl:variable>
+    <xsl:variable name="InductiveTypeDoc" select="document($InductiveTypeUrl)"/>
     <m:apply helm:xref="{@id}">
      <m:csymbol>mutcase</m:csymbol>
      <xsl:apply-templates select="patternsType/*[1]" mode="noannot"/>
      <xsl:apply-templates select="inductiveTerm/*[1]" mode="noannot"/>
-     <xsl:variable name="nop"><xsl:value-of select="document(concat(string($absPath),$Turi))/InductiveDefinition/@noParams"/></xsl:variable>
+     <xsl:variable name="nop"><xsl:value-of select="$InductiveTypeDoc/InductiveDefinition/@noParams"/></xsl:variable>
 <piecewise>
      <xsl:for-each select="pattern">
       <xsl:variable name="pos" select="position()"/>
-      <xsl:variable name="nopar"><xsl:apply-templates select="document(concat(string($absPath),$Turi))/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($pos)]/*[1]" mode="counting"><xsl:with-param name="noparams" select="$nop"/></xsl:apply-templates></xsl:variable>
+      <xsl:variable name="nopar"><xsl:apply-templates select="$InductiveTypeDoc/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($pos)]/*[1]" mode="counting"><xsl:with-param name="noparams" select="$nop"/></xsl:apply-templates></xsl:variable>
 <piece>
       <xsl:apply-templates select="./*[1]" mode="abstparams"><xsl:with-param name="noparams" select="$nopar"/><xsl:with-param name="target" select="1"/><xsl:with-param name="binder">LAMBDA</xsl:with-param></xsl:apply-templates>
 
       <xsl:choose>
       <xsl:when test="$nopar = 0">
        <m:ci>
-        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="document(concat(string($absPath),$Turi))/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($pos)]/@name"/></xsl:with-param></xsl:call-template>
+        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="$InductiveTypeDoc/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($pos)]/@name"/></xsl:with-param></xsl:call-template>
        </m:ci>
       </xsl:when>
       <xsl:otherwise>
        <m:apply>
         <m:csymbol>app</m:csymbol>
         <m:ci>
-         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="document(concat(string($absPath),$Turi))/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($pos)]/@name"/></xsl:with-param></xsl:call-template>
+         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="$InductiveTypeDoc/InductiveDefinition/InductiveType[position()=number($Tindex)+1]/Constructor[position()=number($pos)]/@name"/></xsl:with-param></xsl:call-template>
         </m:ci>
         <xsl:apply-templates select="./*[1]" mode="abstparams"><xsl:with-param name="noparams" select="$nopar"/><xsl:with-param name="binder">LAMBDA</xsl:with-param></xsl:apply-templates>
         </m:apply>

diff --git a/helm/style/drop_coercions.xsl b/helm/style/drop_coercions.xsl
index a259955dd305a38584e7909023846835fc6962ad..9731d6601a29df990ecd9413884d5b0a33e74f2c 100644 (file)
--- a/helm/style/drop_coercions.xsl
+++ b/helm/style/drop_coercions.xsl
@@ -34,7 +34,7 @@
 
 <xsl:param name="CICURI" select="''"/>
 <xsl:param name="getterURL" select="''"/>
-<xsl:variable name="absPath"><xsl:value-of select="$getterURL"/>getxml?uri=</xsl:variable>
+<xsl:include href="getter.xsl"/>
 <xsl:include href="params.xsl"/>
 
 <!-- coercions -->

diff --git a/helm/style/getter.xsl b/helm/style/getter.xsl
new file mode 100644 (file)
index 0000000..c2f36de
--- /dev/null
+++ b/helm/style/getter.xsl
@@ -0,0 +1,34 @@
+<?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/.                                         -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+
+<xsl:template name="URLofURI4getter">
+ <xsl:param name="uri" select="''"/>
+ <xsl:value-of select="$getterURL"/>getxml?uri=<xsl:value-of select="$uri"/>
+</xsl:template>
+
+</xsl:stylesheet>

diff --git a/helm/style/html_set.xsl b/helm/style/html_set.xsl
index 900329f795c394025548cb8e03f6ac2134e450a9..4003d258c48339b7a20b3e1a3fdb64242007a6f8 100644 (file)
--- a/helm/style/html_set.xsl
+++ b/helm/style/html_set.xsl
@@ -110,8 +110,6 @@
 
  <xsl:template mode="inline" match="m:set">
   <xsl:variable name="uri" select="@definitionURL"/>
-<!--   <xsl:value-of select="concat(string($absPath), @definitionURL)"/>
-  </xsl:variable>-->
   <xsl:choose>
    <xsl:when test="count(child::*) = 0">
     <xsl:call-template name="mksymbol">
@@ -294,8 +292,6 @@
   <xsl:param name="current_indent" select="0"/> 
   <xsl:param name="width" select="$framewidth"/>
   <xsl:variable name="uri" select="@definitionURL"/>
-<!--   <xsl:value-of select="concat(string($absPath), @definitionURL)"/>
-  </xsl:variable>-->
   <xsl:choose>
    <xsl:when test="count(child::*) = 0">
     <xsl:call-template name="mksymbol">

diff --git a/helm/style/inductive.xsl b/helm/style/inductive.xsl
index ae225272df0ed758423fcac63b8ba34550e96017..83569d751660cf0008629f29c8986d149b2f0441 100644 (file)
--- a/helm/style/inductive.xsl
+++ b/helm/style/inductive.xsl
@@ -43,8 +43,9 @@
  <xsl:param name="section_params" select="0"/>
  <!-- expected_args_type contains the types of the arguments expected by
       the induction principle -->
+ <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="*[1]/@uri"/></xsl:call-template></xsl:variable>
  <xsl:variable name="expected_args_types" 
-       select="document(concat(string($absPath),*[1]/@uri))/Definition/type//PROD[not(ancestor::source)]/source/*[1]"/>
+       select="document($InductiveTypeUrl)/Definition/type//PROD[not(ancestor::source)]/source/*[1]"/>
  <xsl:variable name="no_expected_args" select="count($expected_args_types)"/>
  <xsl:variable name="actual_arguments" select="*[position()>(1+$section_params)]"/>
  <!-- First check that the induction principle is applied to the

diff --git a/helm/style/objtheorycontent.xsl b/helm/style/objtheorycontent.xsl
index 35444996288a0afe3d1e99a4881b205678992077..7d890d61144fb193247170a1f9ba02aad9f2c8ca 100644 (file)
--- a/helm/style/objtheorycontent.xsl
+++ b/helm/style/objtheorycontent.xsl
@@ -35,11 +35,11 @@
 
 <xsl:import href="objcontent.xsl"/>
 <xsl:include href="headercontent.xsl"/>
+<xsl:include href="getter.xsl"/>
 
 <xsl:param name="type" select="'standalone'"/>
 <xsl:param name="getterURL" select="'http://localhost:8081/'"/>
 <xsl:param name="CICURI" select="''"/>
-<xsl:variable name="absPath"><xsl:value-of select="$getterURL"/>getxml?uri=</xsl:variable>
 
 <!-- CIC DEFINITION -->
 

diff --git a/helm/style/params.xsl b/helm/style/params.xsl
index 6e7f98545509620df3e99d1b9a4dfc7f9ceb5fca..b5b7f9b88ee7357497be3ec9d189cc76bf11245e 100644 (file)
--- a/helm/style/params.xsl
+++ b/helm/style/params.xsl
@@ -165,8 +165,9 @@
      <xsl:choose>
       <xsl:when test="$offset > 0">
        <xsl:variable name="params"> 
+        <xsl:variable name="second_url"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$second_uri"/></xsl:call-template></xsl:variable>
         <xsl:value-of 
-            select="document(concat(string($absPath),$second_uri))/*/@params"/>
+            select="document($second_url)/*/@params"/>
        </xsl:variable>
        <xsl:variable name="minimum">
         <xsl:call-template name="min">

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 51a0f0d52a5abc6b91eff213af41aeaf01049061..0651f65ec6cdb2224b864010bd8a5025953cbee2 100644 (file)
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -108,8 +108,9 @@
       <xsl:when test="contains($uri,'_ind.con')">
        <xsl:variable name="ind_uri" 
          select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
+       <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
        <xsl:variable name="inductive_def" 
-     select="document(concat(string($absPath),$ind_uri))/InductiveDefinition"/>
+     select="document($InductiveTypeUrl)/InductiveDefinition"/>
        <!-- check if the corresponding inductive definition actually
             exists -->
        <xsl:choose>

diff --git a/helm/style/ricerca.xsl b/helm/style/ricerca.xsl
index 9831718df201d8c793f364d7dbc007b2f42e300d..e22a2a943e3e780a16cd1d0f7e9b33d6ed4f3797 100644 (file)
--- a/helm/style/ricerca.xsl
+++ b/helm/style/ricerca.xsl
@@ -31,6 +31,8 @@
 
 <xsl:output method="html"/>
 
+<!-- CSC: absPath is the old way to retrieve a file. The new one is using -->
+<!--  URLofURI4getter, defined in getter.xsl                              -->
 <xsl:variable name="absPath"><xsl:value-of select="$getterURL"/>getxml?uri=</xsl:variable>
 
 <xsl:template match="/">

diff --git a/helm/style/rootcontent.xsl b/helm/style/rootcontent.xsl
index 497e54c48010cd53873237b57f2782337a20d1e7..64acead3600beb66bb1bebb8432deeafc28d96bd 100644 (file)
--- a/helm/style/rootcontent.xsl
+++ b/helm/style/rootcontent.xsl
@@ -45,6 +45,7 @@
 
 <xsl:import href="annotatedcont.xsl"/>
 <xsl:import href="links_library.xsl"/>
+<xsl:import href="getter.xsl"/>
 
 <xsl:param name="getterURL" select="'http://localhost:8081/'"/>
 <xsl:param name="processorURL" select="'http://localhost:8080/helm/servlet/uwobo/'"/>
@@ -52,17 +53,16 @@
 <xsl:param name="annotations" select="'no'"/>
 <xsl:param name="CICURI" select="''"/>
 
-<xsl:variable name="absPath"><xsl:value-of select="$getterURL"/>getxml?uri=</xsl:variable>
-
 <xsl:variable name="InnerTypesUri"><xsl:value-of select="concat($CICURI,'.types')"/></xsl:variable>
+<xsl:variable name="AnnotationsUri"><xsl:value-of select="concat($CICURI,'.ann')"/></xsl:variable>
 
 <xsl:variable name="InnerTypesUrl"><xsl:call-template name="makeURL4InnerTypes"><xsl:with-param name="uri" select="$InnerTypesUri"/></xsl:call-template></xsl:variable>
+<xsl:variable name="AnnotationsUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$AnnotationsUri"/></xsl:call-template></xsl:variable>
 
 <!-- WARNING: Using lazy evaluation: $CICURI.* may not exist, but -->
 <!-- document() is called only by need!!!                         -->
-<!-- <xsl:variable name="InnerTypes" select="document(concat($absPath,$CICURI,'.types'))"/> -->
 <xsl:variable name="InnerTypes" select="document($InnerTypesUrl)"/> 
-<xsl:variable name="CICAnnotations" select="document(concat($absPath,$CICURI,'.ann'))"/> 
+<xsl:variable name="CICAnnotations" select="document($AnnotationsUrl)"/> 
 
 <xsl:include href="headercontent.xsl"/>
 <xsl:include href="proofs.xsl"/>