]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/html_init.xsl
Initial revision
[helm.git] / helm / style / html_init.xsl
diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl
new file mode 100644 (file)
index 0000000..9e81b16
--- /dev/null
@@ -0,0 +1,259 @@
+<?xml version="1.0"?>
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:m="http://www.w3.org/1998/Math/MathML">
+
+<!--***********************************************************************--> 
+<!-- INIT style for HTML                                                   -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
+<!--***********************************************************************--> 
+
+<xsl:variable name="absPath">http://localhost:8081/get?url=</xsl:variable>
+
+
+<!-- BASIC OPERATORS -->
+
+ <xsl:template match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
+       |m:geq|m:gt|m:plus|m:times]">
+  <xsl:param name="current_indent" select="0"/> 
+  <xsl:param name="width" select="$framewidth"/>
+  <xsl:variable name="uri">
+   <xsl:value-of select="*[1]/@definitionURL"/>
+  </xsl:variable>
+  <xsl:variable name="charlength">
+   <xsl:apply-templates select="*[1]" mode="charcount"/>
+  </xsl:variable>
+  <xsl:variable name="symbol">
+   <xsl:choose>
+    <xsl:when test="m:and">
+     <xsl:value-of select="'&#217;'"/>
+    </xsl:when>
+    <xsl:when test="m:or">
+     <xsl:value-of select="'&#218;'"/>
+    </xsl:when>
+    <xsl:when test="m:eq">
+     <xsl:value-of select="'&#61;'"/>
+    </xsl:when>
+    <xsl:when test="m:neq">
+     <xsl:value-of select="'&#185;'"/>
+    </xsl:when>
+    <xsl:when test="m:leq">
+     <xsl:value-of select="'&#163;'"/>
+    </xsl:when>
+    <xsl:when test="m:lt">
+     <xsl:value-of select="'&#60;'"/>
+    </xsl:when>
+    <xsl:when test="m:geq">
+     <xsl:value-of select="'&#179;'"/>
+    </xsl:when>
+    <xsl:when test="m:gt">
+     <xsl:value-of select="'&#62;'"/>
+    </xsl:when>
+    <xsl:when test="m:plus">
+     <xsl:value-of select="'&#43;'"/>
+    </xsl:when>
+    <xsl:when test="m:times">
+     <xsl:value-of select="'&#42;'"/>
+    </xsl:when>
+   </xsl:choose>
+  </xsl:variable>
+  <xsl:choose>
+    <xsl:when test="$charlength > $framewidth">
+     <xsl:text>(</xsl:text>
+     <xsl:apply-templates select="*[2]">
+      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+     </xsl:apply-templates>
+     <BR/> 
+     <xsl:call-template name="make_indent">
+      <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
+     </xsl:call-template>
+     <a>
+     <xsl:attribute name="href">
+      <xsl:value-of select="concat(string($header),string($uri))"/>
+     </xsl:attribute>
+     <FONT FACE="symbol" color="blue">
+      <xsl:value-of select="$symbol"/>
+     </FONT>
+     </a>
+     <xsl:apply-templates select="*[3]">
+      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+     </xsl:apply-templates>
+     <xsl:text>)</xsl:text>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:text>(</xsl:text>
+     <xsl:apply-templates select="*[2]"/>
+     <a>
+     <xsl:attribute name="href">
+      <xsl:value-of select="concat(string($header),string($uri))"/>
+     </xsl:attribute>
+     <FONT FACE="symbol" color="blue">
+     <xsl:value-of select="$symbol"/>
+     </FONT>
+     </a>
+     <xsl:apply-templates select="*[3]"/>
+     <xsl:text>)</xsl:text>
+    </xsl:otherwise>
+   </xsl:choose>
+ </xsl:template>
+
+<!-- MINUS (can be unary!) -->
+
+<xsl:template match="m:apply[m:minus]">
+  <xsl:param name="current_indent" select="0"/> 
+  <xsl:param name="width" select="$framewidth"/>
+  <xsl:variable name="uri">
+   <xsl:value-of select="*[1]/@definitionURL"/>
+  </xsl:variable>
+  <xsl:choose>
+   <xsl:when test="count(child::*)=2">
+    <a>
+    <xsl:attribute name="href">
+     <xsl:value-of select="concat(string($header),string($uri))"/>
+    </xsl:attribute>
+    <xsl:text>-</xsl:text>
+    </a>
+    <xsl:apply-templates select="*[2]">
+     <xsl:with-param name="current_indent" select="$current_indent + 1"/>
+    </xsl:apply-templates>
+   </xsl:when>
+   <xsl:otherwise>
+    <xsl:variable name="charlength">
+     <xsl:apply-templates select="*[1]" mode="charcount"/>
+    </xsl:variable>
+    <xsl:choose>
+     <xsl:when test="$charlength > $framewidth">
+      <xsl:text>(</xsl:text>
+      <xsl:apply-templates select="*[2]">
+       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+      </xsl:apply-templates>
+      <BR/> 
+      <xsl:call-template name="make_indent">
+       <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
+      </xsl:call-template>
+      <a>
+      <xsl:attribute name="href">
+       <xsl:value-of select="concat(string($header),string($uri))"/>
+      </xsl:attribute>
+      <xsl:text>-</xsl:text>
+      </a>
+      <xsl:apply-templates select="*[3]">
+       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+      </xsl:apply-templates>
+      <xsl:text>)</xsl:text>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:text>(</xsl:text>
+      <xsl:apply-templates select="*[2]"/>
+      <a>
+      <xsl:attribute name="href">
+       <xsl:value-of select="concat(string($header),string($uri))"/>
+      </xsl:attribute>
+      <xsl:text>-</xsl:text>
+      </a>
+      <xsl:apply-templates select="*[3]"/>
+      <xsl:text>)</xsl:text>
+     </xsl:otherwise>
+    </xsl:choose>
+   </xsl:otherwise>
+  </xsl:choose>
+ </xsl:template>
+
+<!-- NOT -->
+
+ <xsl:template match="m:apply[m:not]">
+  <xsl:param name="current_indent" select="0"/> 
+  <xsl:param name="width" select="$framewidth"/>
+  <xsl:variable name="uri">
+   <xsl:value-of select="m:not/@definitionURL"/>
+  </xsl:variable>
+     <a>
+     <xsl:attribute name="href">
+      <xsl:value-of select="concat(string($header),string($uri))"/>
+     </xsl:attribute>
+     <FONT FACE="symbol" color="blue">&#216;</FONT>
+     </a>
+     <xsl:apply-templates select="*[2]"/>
+ </xsl:template>
+
+<!-- EXISTS -->
+
+ <xsl:template match="m:apply[m:exists]">
+  <xsl:param name="current_indent" select="0"/> 
+  <xsl:param name="width" select="$framewidth"/>
+  <xsl:variable name="uri">
+   <xsl:value-of select="m:exists/@definitionURL"/>
+  </xsl:variable>
+  <xsl:variable name="charlength">
+   <xsl:apply-templates select="m:exists" mode="charcount"/>
+  </xsl:variable>
+  <xsl:choose>
+    <xsl:when test="$charlength > $framewidth">
+     <a>
+     <xsl:attribute name="href">
+      <xsl:value-of select="concat(string($header),string($uri))"/>
+     </xsl:attribute>
+     <FONT FACE="symbol" color="blue">&#36;</FONT>
+     </a>
+     <xsl:apply-templates select="m:bvar/m:ci"/>
+     <xsl:text>:</xsl:text>
+     <xsl:apply-templates select="m:condition">
+      <xsl:with-param name="current_indent" select="$current_indent + 2 +
+                                string-length(bvar/ci)"/> 
+     </xsl:apply-templates>
+     <BR/> 
+      <xsl:call-template name="make_indent">
+       <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
+      </xsl:call-template>
+     <xsl:text>.</xsl:text>
+      <xsl:apply-templates select="*[last()]">
+       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+      </xsl:apply-templates>
+    </xsl:when>
+    <xsl:otherwise>
+     <a>
+     <xsl:attribute name="href">
+      <xsl:value-of select="concat(string($header),string($uri))"/>
+     </xsl:attribute>
+     <FONT FACE="symbol" color="blue">&#36;</FONT>
+     </a>
+     <xsl:apply-templates select="m:bvar/m:ci"/>
+     <xsl:text>:</xsl:text>
+     <xsl:apply-templates select="m:condition"/>
+     <xsl:text>.</xsl:text>
+     <xsl:apply-templates select="*[last()]">
+      <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+     </xsl:apply-templates>
+    </xsl:otherwise>
+   </xsl:choose>
+ </xsl:template>
+
+
+
+
+<!-- COUNTING -->
+
+<xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:neq
+   |m:lt|m:leq|m:gt|m:geq|m:plus|m:minus|m:times" mode="charcount">
+<xsl:param name="incurrent_length" select="0"/> 
+    <xsl:choose>
+    <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
+     <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/></xsl:apply-templates></xsl:variable>
+     <xsl:choose>
+     <xsl:when test="string($siblength) = &quot;&quot;">
+      <xsl:value-of select="$incurrent_length + string-length()"/>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:value-of select="number($siblength)"/>
+     </xsl:otherwise>
+     </xsl:choose>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:value-of select="$incurrent_length + string-length()"/>
+    </xsl:otherwise>
+    </xsl:choose>
+</xsl:template> 
+
+</xsl:stylesheet> 
+
+