]> matita.cs.unibo.it Git - helm.git/blob - helm/style/annotatedcont.xsl
Initial revision
[helm.git] / helm / style / annotatedcont.xsl
1 <?xml version="1.0"?>
2
3 <!-- Copyright (C) 2000, HELM Team                                     -->
4 <!--                                                                   -->
5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
6 <!-- Library of Mathematics, developed at the Computer Science         -->
7 <!-- Department, University of Bologna, Italy.                         -->
8 <!--                                                                   -->
9 <!-- HELM is free software; you can redistribute it and/or             -->
10 <!-- modify it under the terms of the GNU General Public License       -->
11 <!-- as published by the Free Software Foundation; either version 2    -->
12 <!-- of the License, or (at your option) any later version.            -->
13 <!--                                                                   -->
14 <!-- HELM is distributed in the hope that it will be useful,           -->
15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
17 <!-- GNU General Public License for more details.                      -->
18 <!--                                                                   -->
19 <!-- You should have received a copy of the GNU General Public License -->
20 <!-- along with HELM; if not, write to the Free Software               -->
21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
22 <!-- MA  02111-1307, USA.                                              -->
23 <!--                                                                   -->
24 <!-- For details, see the HELM World-Wide-Web page,                    -->
25 <!-- http://cs.unibo.it/helm/.                                         -->
26
27 <!--***********************************************************************--> 
28 <!-- XSLT version 0.1 of annotated MathML content to MathML presentation:  -->
29 <!-- First draft: March 29 2000, Claudio Sacerdoti Coen, Irene Schena      -->
30 <!--***********************************************************************--> 
31
32 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
33                               xmlns:m="http://www.w3.org/1998/Math/MathML"
34                               xmlns:helm="http://www.cs.unibo.it/helm">
35
36 <xsl:import href="objcontent.xsl"/>
37
38 <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"/>
39
40 <xsl:template match="Definition|Axiom|CurrentProof|InductiveDefinition|Variable">
41     <xsl:variable name="id" select="@id"/>
42     <xsl:choose>
43     <xsl:when test="$annotations='yes' and $CICAnnotations/Annotations/Annotation[@of=$id]">
44      <annotation helm:xref="{@id}">
45       <xsl:apply-templates select="$CICAnnotations/Annotations/Annotation[@of=$id]"/>
46      </annotation>
47     </xsl:when>
48     <xsl:otherwise>
49      <xsl:apply-templates select="." mode="noannot"/>
50     </xsl:otherwise>
51     </xsl:choose>
52 </xsl:template>
53
54 <xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX">
55     <xsl:variable name="id" select="@id"/>
56     <xsl:choose>
57     <xsl:when test="$annotations='yes' and $CICAnnotations/Annotations/Annotation[@of=$id]">
58      <annotation helm:xref="{@id}">
59       <xsl:apply-templates select="$CICAnnotations/Annotations/Annotation[@of=$id]"/>
60      </annotation>
61     </xsl:when>
62     <xsl:otherwise>
63      <m:math>
64       <xsl:apply-templates select="." mode="noannot"/>
65      </m:math>
66     </xsl:otherwise>
67     </xsl:choose>
68 </xsl:template>
69
70 <!-- The next two templates must be invoked with the context node -->
71 <!-- belonging to the original document DOM tree                  -->
72
73 <xsl:template mode="changecontextdocumentnode" match="*">
74  <xsl:param name="id" select="''"/>
75  <xsl:apply-templates select="key('id',$id)"/>
76 </xsl:template>
77
78 <xsl:template mode="changecontextdocumentattribute" match="*">
79  <xsl:param name="id" select="''"/>
80  <xsl:param name="name" select="''"/>
81  <xsl:param name="child" select="''"/>
82  <xsl:param name="grandchild" select="''"/>
83  <xsl:choose>
84   <xsl:when test="$child">
85    <xsl:choose>
86     <xsl:when test="$grandchild">
87      <xsl:value-of select="key('id',$id)/*[position() = $child]/*[position() = $grandchild]/attribute::*[name() = $name]"/>
88     </xsl:when>
89     <xsl:otherwise>
90      <xsl:value-of select="key('id',$id)/*[position() = $child]/attribute::*[name() = $name]"/>
91     </xsl:otherwise>
92    </xsl:choose>
93   </xsl:when>
94   <xsl:otherwise>
95    <xsl:value-of select="key('id',$id)/attribute::*[name() = $name]"/>
96   </xsl:otherwise>
97  </xsl:choose>
98 </xsl:template>
99
100 <!-- $cicroot holds the root of the original document DOM tree  -->
101 <!-- The next two templates are trampolines to the previous two -->
102 <!-- that are used to change the context node to a node in the  -->
103 <!-- document DOM tree of $cicroot                              -->
104
105 <xsl:variable name="cicroot" select="/"/>
106
107 <xsl:template match="node">
108  <xsl:apply-templates select="$cicroot/*[1]" mode="changecontextdocumentnode">
109   <xsl:with-param name="id" select="@id"/>
110  </xsl:apply-templates>
111 </xsl:template>
112
113 <xsl:template match="attribute">
114  <xsl:apply-templates select="$cicroot/*[1]" mode="changecontextdocumentattribute">
115   <xsl:with-param name="id" select="@id"/>
116   <xsl:with-param name="name" select="@name"/>
117   <xsl:with-param name="child" select="@child"/>
118   <xsl:with-param name="grandchild" select="@grandchild"/>
119  </xsl:apply-templates>
120 </xsl:template>
121
122 </xsl:stylesheet>