From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 16 Mar 2001 17:27:33 +0000 (+0000)
Subject: Annotations now working again (even if in a bit trickier way).
X-Git-Tag: v0_1_2~68
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=699fe34e458506db3ade298abc8c64cf622d27ba;p=helm.git

Annotations now working again (even if in a bit trickier way).
The get method of the getter could now be safely removed... URRAH!
---

diff --git a/helm/style/annotatedcont.xsl b/helm/style/annotatedcont.xsl
index 7d5a6d5b3..97f259d67 100644
--- a/helm/style/annotatedcont.xsl
+++ b/helm/style/annotatedcont.xsl
@@ -37,13 +37,12 @@
 
 <xsl:key name="id" use="@id" match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|Definition|Axiom|CurrentProof|InductiveDefinition|Variable"/>
 
-<xsl:key name="annid" use="@of" match="Annotation"/>
-
 <xsl:template match="Definition|Axiom|CurrentProof|InductiveDefinition|Variable">
+    <xsl:variable name="id" select="@id"/>
     <xsl:choose>
-    <xsl:when test="key('annid',@id)">
+    <xsl:when test="$annotations='yes' and $CICAnnotations/Annotations/Annotation[@of=$id]">
      <annotation helm:xref="{@id}">
-      <xsl:apply-templates select="key('annid',@id)"/>
+      <xsl:apply-templates select="$CICAnnotations/Annotations/Annotation[@of=$id]"/>
      </annotation>
     </xsl:when>
     <xsl:otherwise>
@@ -53,10 +52,11 @@
 </xsl:template>
 
 <xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX">
+    <xsl:variable name="id" select="@id"/>
     <xsl:choose>
-    <xsl:when test="key('annid',@id)">
+    <xsl:when test="$annotations='yes' and $CICAnnotations/Annotations/Annotation[@of=$id]">
      <annotation helm:xref="{@id}">
-      <xsl:apply-templates select="key('annid',@id)"/>
+      <xsl:apply-templates select="$CICAnnotations/Annotations/Annotation[@of=$id]"/>
      </annotation>
     </xsl:when>
     <xsl:otherwise>
@@ -67,16 +67,19 @@
     </xsl:choose>
 </xsl:template>
 
-<xsl:template match="node">
- <xsl:variable name="id" select="@id"/>
+<!-- The next two templates must be invoked with the context node -->
+<!-- belonging to the original document DOM tree                  -->
+
+<xsl:template mode="changecontextdocumentnode" match="*">
+ <xsl:param name="id" select="''"/>
  <xsl:apply-templates select="key('id',$id)"/>
 </xsl:template>
 
-<xsl:template match="attribute">
- <xsl:variable name="id" select="@id"/>
- <xsl:variable name="name" select="@name"/>
- <xsl:variable name="child" select="@child"/>
- <xsl:variable name="grandchild" select="@grandchild"/>
+<xsl:template mode="changecontextdocumentattribute" match="*">
+ <xsl:param name="id" select="''"/>
+ <xsl:param name="name" select="''"/>
+ <xsl:param name="child" select="''"/>
+ <xsl:param name="grandchild" select="''"/>
  <xsl:choose>
   <xsl:when test="$child">
    <xsl:choose>
@@ -94,4 +97,26 @@
  </xsl:choose>
 </xsl:template>
 
+<!-- $cicroot holds the root of the original document DOM tree  -->
+<!-- The next two templates are trampolines to the previous two -->
+<!-- that are used to change the context node to a node in the  -->
+<!-- document DOM tree of $cicroot                              -->
+
+<xsl:variable name="cicroot" select="/"/>
+
+<xsl:template match="node">
+ <xsl:apply-templates select="$cicroot/*[1]" mode="changecontextdocumentnode">
+  <xsl:with-param name="id" select="@id"/>
+ </xsl:apply-templates>
+</xsl:template>
+
+<xsl:template match="attribute">
+ <xsl:apply-templates select="$cicroot/*[1]" mode="changecontextdocumentattribute">
+  <xsl:with-param name="id" select="@id"/>
+  <xsl:with-param name="name" select="@name"/>
+  <xsl:with-param name="child" select="@child"/>
+  <xsl:with-param name="grandchild" select="@grandchild"/>
+ </xsl:apply-templates>
+</xsl:template>
+
 </xsl:stylesheet>
diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 533cf2299..74d6505bf 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -36,10 +36,11 @@
 <xsl:param name="processorURL" select="'http://localhost:8080/helm/servlet/uwobo/'"/>
 <xsl:param name="keys" select="'C1,HC2'"/>
 <xsl:param name="naturalLanguage" select="'yes'"/>
+<xsl:param name="annotations" select="'no'"/>
 
 <xsl:variable name="absPath"><xsl:value-of select="$getterURL"/>getciconly?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.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="$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:include href="html_init.xsl"/>
 <xsl:include href="html_set.xsl"/>
diff --git a/helm/style/expandobj.xsl b/helm/style/expandobj.xsl
index d380be3ed..b42afa966 100644
--- a/helm/style/expandobj.xsl
+++ b/helm/style/expandobj.xsl
@@ -39,10 +39,11 @@
 <!-- Keys contains the keys of the stylesheets to be applied -->
 <xsl:param name="keys" select="'C1,C2'"/>
 <xsl:param name="naturalLanguage" select="'yes'"/>
+<xsl:param name="annotations" select="'no'"/>
 
 <xsl:variable name="absPath"><xsl:value-of select="$getterURL"/>getciconly?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.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="$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:output 
 	method="xml"
diff --git a/helm/style/rootcontent.xsl b/helm/style/rootcontent.xsl
index e4bccecea..34a97ab2d 100644
--- a/helm/style/rootcontent.xsl
+++ b/helm/style/rootcontent.xsl
@@ -45,23 +45,23 @@
 
 <xsl:param name="getterURL" select="'http://localhost:8081/'"/>
 <xsl:param name="naturalLanguage" select="'yes'"/>
+<xsl:param name="annotations" select="'no'"/>
 <xsl:param name="CICURI" select="''"/>
 
 <xsl:variable name="absPath"><xsl:value-of select="$getterURL"/>getciconly?uri=</xsl:variable>
 
-<!-- WARNING: Using lazy evaluation: $CICURI.types may not exist, but -->
-<!-- document() is called only by need!!!                             -->
+<!-- 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="CICAnnotations" select="document(concat($absPath,$CICURI,'.ann'))"/>
 
 <xsl:import href="annotatedcont.xsl"/>
-<xsl:key name="id" use="@id" match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|Definition|Axiom|CurrentProof|InductiveDefinition|Variable"/>
+
 <xsl:include href="basic.xsl"/>
 <xsl:include href="set.xsl"/>
 <xsl:include href="reals.xsl"/>
 <xsl:include href="proofs.xsl"/>
 
 <xsl:variable name="showproof" select="0"/>
-</xsl:stylesheet>
-
-
 
+</xsl:stylesheet>