First commit of the NuPRL stylesheets.

[helm.git] / helm / nuprl_stylesheets / nuprl_expand.xsl

diff --git a/helm/nuprl_stylesheets/nuprl_expand.xsl b/helm/nuprl_stylesheets/nuprl_expand.xsl
new file mode 100644 (file)
index 0000000..c31b479
--- /dev/null
+++ b/helm/nuprl_stylesheets/nuprl_expand.xsl
@@ -0,0 +1,108 @@
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:m="http://www.w3.org/1998/Math/MathML"
+                              xmlns:xlink="http://www.w3.org/1999/xlink">
+
+<xsl:key name="sequent" use="m:mtr/m:mtd/m:mrow/m:mtext/text()" match="m:mtable[starts-with(m:mtr/m:mtd/m:mrow/m:mtext/text(),'Sequent (')]"/>
+
+<xsl:template match="/">
+    <xsl:apply-templates select="*"/>
+</xsl:template>
+
+<xsl:template match="m:mi">
+ <xsl:param name="sequentno" select="'/..'"/>
+    <xsl:choose>
+    <xsl:when test="contains(.,'%')">
+    <xsl:variable name="var" select="."/>
+     <m:maction actiontype="toggle">
+      <m:mi mathcolor="green"><xsl:value-of select="."/></m:mi>
+      <m:mrow>
+       <m:mi mathcolor="green"><xsl:value-of select="$var"/>: </m:mi>
+       <xsl:call-template name="look_for_decl">
+        <xsl:with-param name="csequent" select="$sequentno"/>
+        <xsl:with-param name="var" select="$var"/>
+       </xsl:call-template>
+      </m:mrow>
+     </m:maction>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:copy>
+      <xsl:apply-templates select="@*|node()"/>
+     </xsl:copy>
+    </xsl:otherwise>
+    </xsl:choose>
+</xsl:template>
+
+<xsl:template match="m:mtable[starts-with(m:mtr/m:mtd/m:mrow/m:mtext/text(),'Sequent')]">
+ <xsl:copy>
+  <xsl:variable name="text" select="m:mtr/m:mtd/m:mrow/m:mtext/text()"/>
+  <xsl:variable name="tmp1" select="substring-after($text,'Sequent (')"/>
+  <xsl:variable name="tmp2" select="substring-before($tmp1,')')"/>
+  <xsl:apply-templates select="*|@*|text()">
+   <xsl:with-param name="sequentno" select="$tmp2"/>
+  </xsl:apply-templates>
+ </xsl:copy>
+</xsl:template>
+
+<xsl:template match="*|@*|text()">
+ <xsl:param name="sequentno" select="'/..'"/> 
+ <xsl:copy>
+  <xsl:apply-templates select="*|@*|text()">
+   <xsl:with-param name="sequentno" select="$sequentno"/>
+  </xsl:apply-templates>
+ </xsl:copy>
+</xsl:template>
+
+<xsl:template name="look_for_decl">
+   <xsl:param name="csequent" select="/.."/>
+   <xsl:param name="var" select="''"/>
+   <xsl:param name="result" select="0"/>
+   <xsl:choose>
+   <xsl:when test="$csequent=''">
+        <m:mi>
+        ERROR
+       </m:mi>
+   </xsl:when>
+   <xsl:otherwise>
+    <xsl:variable name="sect_table" select="key('sequent',concat('Sequent (',$csequent,')'))"/>
+    <xsl:variable name="check_res" select="$sect_table/m:mtr/m:mtable/m:mtr/m:mtd/m:mrow/m:mo[text()=$var]/following-sibling::*[2]"/>
+     <xsl:choose>
+     <xsl:when test="not ($check_res)">
+      <xsl:variable name="new_sequent">
+       <xsl:call-template name="truncate">
+        <xsl:with-param name="tail" select="$csequent"/>
+       </xsl:call-template>
+      </xsl:variable>
+      <xsl:call-template name="look_for_decl">
+       <xsl:with-param name="csequent" select="$new_sequent"/>
+       <xsl:with-param name="var" select="$var"/>
+      </xsl:call-template>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:copy-of select="$check_res"/>
+     </xsl:otherwise>
+     </xsl:choose>
+   </xsl:otherwise>
+   </xsl:choose>
+</xsl:template>
+
+<xsl:template name="truncate">
+ <xsl:param name="tail" select="''"/>
+ <xsl:param name="head" select="''"/>
+ <xsl:choose>
+ <xsl:when test="substring-before($tail,' ')=''">
+  <xsl:value-of select="$head"/>
+ </xsl:when>
+ <xsl:otherwise>
+  <xsl:variable name="head1">
+   <xsl:if test="$head !=''">
+    <xsl:value-of select="concat($head,' ')"/>
+   </xsl:if>
+  </xsl:variable>
+  <xsl:call-template name="truncate">
+   <xsl:with-param name="tail" select="substring-after($tail,' ')"/>
+   <xsl:with-param name="head" select="concat($head1,substring-before($tail,' '))"/>
+  </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+</xsl:stylesheet>