--- /dev/null
+H=@
+
+TAGS = lint-xml index lddl install-xml \
+ test-html html install-html \
+ install-jed install-bib
+
+LDDLURL = http://lambda-delta.info/static/lddl
+
+ETCDIR = etc
+DOWNDIR = download
+XSLTDIR = xslt
+XMLDIR = xml
+HTMLDIR = $(HOME)/public_html/lddl
+JEDDIR = $(HOME)/mps/jed
+BIBDIR = $(HOME)/texmf/bibtex/bib
+
+RXMLDIR = helm:/projects/helm/public_html/lambda_delta/xml
+RHTMLDIR = helm:/projects/helm/public_html/lambda_delta/static/lddl
+
+SLS = helena.sl automath.sl
+BIB = lambda_delta.bib
+
+XMLS = brg_si/grundlagen/l/not.ld.xml \
+ brg_si/grundlagen/l/et.ld.xml \
+ brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
+ brg_si/grundlagen/l/e/pairis1.ld.xml \
+ brg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
+ crg_si/grundlagen/l/not.ld.xml \
+ crg_si/grundlagen/l/et.ld.xml \
+ crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
+ crg_si/grundlagen/l/e/pairis1.ld.xml \
+ crg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
+ brg_si/grundlagen/ccs.ldc.xml
+
+XMLLINT = xmllint --noout
+XSLT = xsltproc
+
+lint-xml: $(XMLS:%=$(XMLDIR)/%)
+ @echo XMLLINT --valid
+ $(H)$(XMLLINT) --valid $^
+
+$(ETCDIR)/make-html.sh $(XMLDIR)/index.txt index:
+ @echo " GENERATE INDEXES"
+ $(H)find $(XMLDIR) -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > $(XMLDIR)/index.txt
+ $(H)sed "s/^/make --no-print-directory /" $(XMLDIR)/index.txt | sed s.ld:/.. > $(ETCDIR)/make_html.sh
+
+lddl: $(ETCDIR)/exclude.txt index
+ @echo " GENERATE lddl.tar.bz2"
+ $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X $< $(XMLDIR)
+
+install-xml: $(XMLDIR)/index.txt
+ @echo " INSTALL xml"
+ $(H)scp -r $< $(XMLDIR)/brg_si/ $(XMLDIR)/crg_si/ $(RXMLDIR)
+
+test-html:
+ @$(MAKE) --no-print-directory $(XMLS:%.xml=%)
+
+html: $(ETCDIR)/make-html.sh
+ @echo " MAKE */*.ld"
+ $(H). $<
+
+install-html: $(ETCDIR)/make_html.sh
+ @echo " INSTALL html"
+ $(H)scp -r $(HTMLDIR)/* $(RHTMLDIR)
+
+install-jed: $(SLS:%=$(JEDDIR)/%)
+ @echo " INSTALL $(SLS)"
+ $(H)scp $(SLS:%=$(JEDDIR)/%) $(DOWNDIR)
+
+install-bib: $(BIB:%=$(BIBDIR)/%)
+ @echo " INSTALL $(BIB)"
+ $(H)scp $< $(DOWNDIR)
+ $(H)scp $< $(DOWNDIR)/$(BIB:%.bib=%.txt)
+
+%.ld: BASEURL = --stringparam baseurl $(LDDLURL)
+
+%.ld:
+ @echo " XSLT $@"
+ $(H)mkdir -p $(HTMLDIR)/$(@D)
+ $(H)$(XSLT) -o $(HTMLDIR)/$@.html $(BASEURL) $(XSLTDIR)/lddl.xsl $(XMLDIR)/$@.xml
+
+%.ldc:
+ @echo " SKIP $@"
--- /dev/null
+@charset "UTF-8";
+
+/* general ******************************************************************/
+
+body {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 0, 0);
+ margin: 2.5%;
+}
+
+a:link, a:visited {
+ text-decoration: underline;
+}
+
+a:active, a:hover, a:focus {
+ background: rgb(192, 192, 192);
+}
+
+/* blocks *******************************************************************/
+
+.spacer {
+ text-align: center;
+}
+
+.head1 {
+ margin: 0.5em 0;
+ text-align: center;
+ font-weight: bold;
+ font-size: xx-large;
+}
+
+.head2 {
+ margin: 0.5em 0;
+ text-align: left;
+ font-weight: bold;
+ font-size: x-large;
+}
+
+.text {
+ margin: 1em 0;
+ text-align: left;
+}
+
+/* inline decorations *******************************************************/
+
+.icon32 {
+ border: 0;
+ width: 32px;
+ height: 32px;
+}
+
+.rule {
+ border: 0;
+ height: 4px;
+ width: 100%;
+}
+
+.w3c {
+ margin: 0 0.5em;
+ border: 0;
+ width: 88px;
+ height: 32px; /* this should be 31px */
+}
--- /dev/null
+@charset "UTF-8";
+
+/* terms ********************************************************************/
+
+.separator {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 0, 0);
+}
+
+.sort {
+ background: rgb(255, 255, 255);
+ color: rgb(128, 0, 255);
+}
+
+.lref {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 0, 0);
+}
+
+.gref {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 0, 255);
+}
+
+.appl {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 0, 0);
+}
+
+.cast {
+ background: rgb(255, 255, 255);
+ color: rgb(255, 0, 0);
+}
+
+.local {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 160, 0);
+}
+
+.global {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 0, 0);
+}
@misc{lambdadelta1,
author="F. {Guidi}",
- title="{lambda-delta}",
- howpublished="Formal specification with the proof assistant \textsc{coq} 7.3.1",
+ title="{lambda\_delta\_1}",
+ howpublished="Formal specification with the proof assistant Coq 7.3.1",
year="2007",
month="January",
- note="Available at the lambda-delta Web site: {http://helm.cs.unibo.it/lambda-delta/}"
+ note="Available at the lambda\_delta Web site: {http://lambda-delta.info/}"
}
@misc{lambdadelta1,
author="F. {Guidi}",
- title="{lambda-delta}",
- howpublished="Formal specification with the proof assistant \textsc{coq} 7.3.1",
+ title="{lambda\_delta\_1}",
+ howpublished="Formal specification with the proof assistant Coq 7.3.1",
year="2007",
month="January",
- note="Available at the lambda-delta Web site: {http://helm.cs.unibo.it/lambda-delta/}"
+ note="Available at the lambda\_delta Web site: {http://lambda-delta.info/}"
}
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!-- DTD for persistent lambda_delta logical data -->
+
+<!-- TERMS -->
+
+<!ENTITY % leaf '(Sort|LRef|GRef)'>
+
+<!ENTITY % node '(Cast|Appl|Abst|Abbr|Void)'>
+
+<!ENTITY % term '(%node;*,%leaf;)'>
+
+<!ENTITY % terms '(%term;*)'>
+
+<!ELEMENT Sort EMPTY>
+<!ATTLIST Sort
+ position NMTOKEN #REQUIRED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT LRef EMPTY>
+<!ATTLIST LRef
+ position NMTOKEN #REQUIRED
+ offset NMTOKEN #IMPLIED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT GRef EMPTY>
+<!ATTLIST GRef
+ uri CDATA #REQUIRED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT Cast %term;>
+<!ATTLIST Cast
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT Appl %terms;>
+<!ATTLIST Appl
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT Abst %terms;>
+<!ATTLIST Abst
+ level NMTOKEN #IMPLIED
+ name NMTOKENS #IMPLIED
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT Abbr %terms;>
+<!ATTLIST Abbr
+ name NMTOKENS #IMPLIED
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT Void EMPTY>
+<!ATTLIST Void
+ name NMTOKENS #IMPLIED
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!-- ENVIRONMENT ENTRIES -->
+
+<!ENTITY % entity '(ABST|ABBR)'>
+
+<!ELEMENT ABST %term;>
+<!ATTLIST ABST
+ uri CDATA #REQUIRED
+ level NMTOKEN #IMPLIED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta NMTOKENS #IMPLIED
+ lang NMTOKEN "en-US"
+ info CDATA #IMPLIED
+>
+
+<!ELEMENT ABBR %term;>
+<!ATTLIST ABBR
+ uri CDATA #REQUIRED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta NMTOKENS #IMPLIED
+ lang NMTOKEN "en-US"
+ info CDATA #IMPLIED
+>
+
+<!ELEMENT ENTITY %entity;>
+<!ATTLIST ENTITY
+ xmlns CDATA #FIXED "http://lambda_delta.info"
+ hierarchy NMTOKEN #REQUIRED
+ options NMTOKENS #IMPLIED
+>
+
+<!-- CONVERSION CONSTRAINT SYSTEM -->
+
+<!ENTITY % cc '(ToPositive|ToOne|ToNext)'>
+
+<!ENTITY % ccs '(%cc;*)'>
+
+<!ELEMENT ToPositive EMPTY>
+<!ATTLIST ToPositive
+ arity NMTOKEN #IMPLIED
+ mark NMTOKENS #IMPLIED
+>
+
+<!ELEMENT ToOne EMPTY>
+<!ATTLIST ToOne
+ arity NMTOKEN #IMPLIED
+ mark NMTOKENS #IMPLIED
+>
+
+<!ELEMENT ToNext EMPTY>
+<!ATTLIST ToNext
+ arity NMTOKEN #IMPLIED
+ prec NMTOKENS #IMPLIED
+ next NMTOKENS #IMPLIED
+>
+
+<!ELEMENT CCS %ccs;>
+<!ATTLIST CCS
+ xmlns CDATA #FIXED "http://lambda_delta.info"
+ uri CDATA #REQUIRED
+>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:param name="baseurl"/>
+
+<xsl:include href="lddl_library.xsl"/>
+<xsl:include href="lddl_term.xsl"/>
+<xsl:include href="lddl_entity.xsl"/>
+<xsl:include href="lddl_root.xsl"/>
+
+<xsl:output
+ method="xml"
+ doctype-public="-//W3C//DTD XHTML 1.1//EN"
+ doctype-system="http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd"
+ encoding="UTF-8"
+ indent="no"
+/>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:strip-space elements="ABST ABBR"/>
+
+<xsl:template name="ENTITY">
+ <xsl:param name="kind"/>
+ <div class="head2">
+ <span class="global">
+ <xsl:value-of select="$kind"/>
+ <xsl:call-template name="cn"/>
+ <xsl:call-template name="sp"/>
+ <span class="gref">
+ <xsl:call-template name="global"/>
+ </span>
+ <xsl:call-template name="sp"/>
+ <xsl:call-template name="op"/>
+ <span class="gref">
+ <xsl:call-template name="mk_path"/>
+ </span>
+ <xsl:call-template name="cp"/>
+ </span>
+ </div>
+ <div class="text">
+ <xsl:call-template name="idescr"/>
+ <xsl:call-template name="qt"/>
+ <xsl:value-of select="@meta"/>
+ <xsl:call-template name="qt"/>
+ </div>
+ <div class="text">
+ <xsl:apply-templates/>
+ </div>
+</xsl:template>
+
+<xsl:template match="ABST">
+ <xsl:call-template name="ENTITY">
+ <xsl:with-param name="kind">Declaration</xsl:with-param>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="ABBR">
+ <xsl:call-template name="ENTITY">
+ <xsl:with-param name="kind">Definition</xsl:with-param>
+ </xsl:call-template>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:template name="sp">
+ <xsl:text> </xsl:text>
+</xsl:template>
+
+<xsl:template name="cm">
+ <xsl:text>, </xsl:text>
+</xsl:template>
+
+<xsl:template name="sl">
+ <xsl:text>/</xsl:text>
+</xsl:template>
+
+<xsl:template name="plus">
+ <xsl:text>+</xsl:text>
+</xsl:template>
+
+<xsl:template name="fs">
+ <xsl:text>.​</xsl:text>
+</xsl:template>
+
+<xsl:template name="op">
+ <xsl:text>(</xsl:text>
+</xsl:template>
+
+<xsl:template name="cp">
+ <xsl:text>)</xsl:text>
+</xsl:template>
+
+<xsl:template name="ob">
+ <xsl:text>[</xsl:text>
+</xsl:template>
+
+<xsl:template name="cb">
+ <xsl:text>]</xsl:text>
+</xsl:template>
+
+<xsl:template name="oa">
+ <xsl:text><</xsl:text>
+</xsl:template>
+
+<xsl:template name="ca">
+ <xsl:text>></xsl:text>
+</xsl:template>
+
+<xsl:template name="cn">
+ <xsl:text>:</xsl:text>
+</xsl:template>
+
+<xsl:template name="eq">
+ <xsl:text>=</xsl:text>
+</xsl:template>
+
+<xsl:template name="qt">
+ <xsl:text>"</xsl:text>
+</xsl:template>
+
+<xsl:template name="idescr">
+ <xsl:text>Informal description: </xsl:text>
+</xsl:template>
+
+<xsl:template name="vpars">
+ <xsl:text>Validation parameters: </xsl:text>
+</xsl:template>
+
+<xsl:template name="shier">
+ <xsl:text>sort hierarchy = </xsl:text>
+</xsl:template>
+
+<xsl:template name="kopts">
+ <xsl:text>kernel options = </xsl:text>
+</xsl:template>
+
+<xsl:template name="multiple">
+ <span class="separator">
+ <xsl:call-template name="cm"/>
+ </span>
+</xsl:template>
+
+<xsl:template name="lambda">
+ <a title="{@mark}">
+ <xsl:choose>
+ <xsl:when test="@level=0">
+ <xsl:text disable-output-escaping="yes">&Pi;</xsl:text>
+ <sup><xsl:value-of select="@level"/></sup>
+ </xsl:when>
+ <xsl:when test="@level=1">
+ <xsl:text disable-output-escaping="yes">&Pi;</xsl:text>
+ </xsl:when>
+ <xsl:when test="@level=2">
+ <xsl:text disable-output-escaping="yes">&lambda;</xsl:text>
+ </xsl:when>
+ <xsl:when test="not(@level)">
+ <xsl:text disable-output-escaping="yes">&lambda;</xsl:text>
+ <sup><xsl:text disable-output-escaping="yes">&infin;</xsl:text></sup>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text disable-output-escaping="yes">&lambda;</xsl:text>
+ <sup><xsl:value-of select="@level"/></sup>
+ </xsl:otherwise>
+ </xsl:choose>
+ </a>
+</xsl:template>
+
+<xsl:template name="delta">
+ <a title="{@mark}">
+ <xsl:text disable-output-escaping="yes">&delta;</xsl:text>
+ </a>
+</xsl:template>
+
+<xsl:template name="chi">
+ <a title="{@mark}">
+ <xsl:text disable-output-escaping="yes">&chi;</xsl:text>
+ </a>
+</xsl:template>
+
+<xsl:template name="position">
+ <xsl:variable name="index">
+ <xsl:value-of select="@position"/>
+ <xsl:if test="@offset != 0">
+ <xsl:call-template name="plus"/>
+ <xsl:value-of select="@offset"/>
+ </xsl:if>
+ </xsl:variable>
+ <a title="{$index}">
+ <xsl:value-of select="@name"/>
+ </a>
+</xsl:template>
+
+<xsl:template name="uri">
+ <xsl:variable name="url">
+ <xsl:value-of select="$baseurl"/>
+ <xsl:value-of select="substring-after(@uri,'ld:')"/>
+ <xsl:text>.html</xsl:text>
+ </xsl:variable>
+ <a href="{$url}" title="{@uri}"><xsl:value-of select="@name"/></a>
+</xsl:template>
+
+<xsl:template name="global">
+ <a title="{@mark}">
+ <xsl:value-of select="@name"/>
+ </a>
+</xsl:template>
+
+<xsl:template name="mk_names">
+ <xsl:param name="names">
+ <xsl:value-of select="normalize-space(@name)"/>
+ <xsl:call-template name="sp"/>
+ </xsl:param>
+ <xsl:param name="sep" select="false()"/>
+ <xsl:if test="$names and $sep">
+ <xsl:call-template name="multiple"/>
+ </xsl:if>
+ <xsl:if test="$names">
+ <span class="lref">
+ <xsl:value-of select="substring-before($names, ' ')"/>
+ </span>
+ <xsl:call-template name="mk_names">
+ <xsl:with-param name="names" select="substring-after($names, ' ')"/>
+ <xsl:with-param name="sep" select="true()"/>
+ </xsl:call-template>
+ </xsl:if>
+</xsl:template>
+
+<xsl:template name="mk_terms">
+ <xsl:for-each select="*">
+ <xsl:apply-templates select="."/>
+ <xsl:if test="(name()='Sort' or name()='LRef' or name()='GRef') and position()!=last()">
+ <xsl:call-template name="multiple"/>
+ </xsl:if>
+ </xsl:for-each>
+</xsl:template>
+
+<xsl:template name="mk_binder">
+ <xsl:param name="sep-seq"/>
+ <xsl:call-template name="ob"/>
+ <xsl:call-template name="mk_binder_rec1">
+ <xsl:with-param name="sep-seq" select="$sep-seq"/>
+ </xsl:call-template>
+ <xsl:call-template name="cb"/>
+</xsl:template>
+
+<xsl:template name="mk_binder_rec1">
+ <xsl:param name="sep-seq"/>
+ <xsl:param name="names">
+ <xsl:value-of select="normalize-space(@name)"/>
+ <xsl:call-template name="sp"/>
+ </xsl:param>
+ <xsl:param name="sep" select="false()"/>
+ <xsl:param name="start" select="true()"/>
+ <xsl:param name="pos" select="1"/>
+ <xsl:choose>
+ <xsl:when test="$start and $pos <= count(*)">
+ <xsl:if test="$names and $sep">
+ <xsl:call-template name="multiple"/>
+ </xsl:if>
+ <span class="lref">
+ <xsl:value-of select="substring-before($names, ' ')"/>
+ </span>
+ <xsl:copy-of select="$sep-seq"/>
+ <xsl:call-template name="mk_binder_rec2">
+ <xsl:with-param name="names" select="substring-after($names, ' ')"/>
+ <xsl:with-param name="pos" select="$pos"/>
+ <xsl:with-param name="sep-seq" select="$sep-seq"/>
+ </xsl:call-template>
+ </xsl:when>
+ <xsl:when test="not($start) and $pos <= count(*)">
+ <xsl:call-template name="mk_binder_rec2">
+ <xsl:with-param name="names" select="$names"/>
+ <xsl:with-param name="pos" select="$pos"/>
+ <xsl:with-param name="sep-seq" select="$sep-seq"/>
+ </xsl:call-template>
+ </xsl:when>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template name="mk_binder_rec2">
+ <xsl:param name="sep-seq"/>
+ <xsl:param name="names"/>
+ <xsl:param name="pos"/>
+ <xsl:apply-templates select="*[$pos]"/>
+ <xsl:call-template name="mk_binder_rec1">
+ <xsl:with-param name="sep-seq" select="$sep-seq"/>
+ <xsl:with-param name="names" select="$names"/>
+ <xsl:with-param name="sep" select="true()"/>
+ <xsl:with-param name="start" select="name(*[$pos])='Sort' or name(*[$pos])='LRef' or name(*[$pos])='GRef'"/>
+ <xsl:with-param name="pos" select="$pos+1"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template name="mk_segment">
+ <xsl:param name="path"/>
+ <xsl:param name="name"/>
+ <xsl:variable name="url">
+ <xsl:value-of select="$baseurl"/>
+ <xsl:value-of select="substring-after($path,'ld:')"/>
+ </xsl:variable>
+ <a href="{$url}"><xsl:value-of select="$name"/></a>
+ <xsl:call-template name="sl"/>
+</xsl:template>
+
+<xsl:template name="mk_path">
+ <xsl:param name="rpath" select="@uri"/>
+ <xsl:variable name="newrpath" select="substring-after($rpath,'/')"/>
+ <xsl:choose>
+ <xsl:when test="$newrpath">
+ <xsl:variable name="segment" select="substring-before($rpath,$newrpath)"/>
+ <xsl:call-template name="mk_segment">
+ <xsl:with-param name="path" select="substring-before(@uri,$newrpath)"/>
+ <xsl:with-param name="name" select="substring-before($segment,'/')"/>
+ </xsl:call-template>
+ <xsl:call-template name="mk_path">
+ <xsl:with-param name="rpath" select="$newrpath"/>
+ </xsl:call-template>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:variable name="path" select="substring-before(@uri,$rpath)"/>
+ <xsl:value-of select="substring-after(@uri,$path)"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template name="lddl">
+ <xsl:text disable-output-escaping="yes">&lambda;&delta; Digital Library (LDDL)</xsl:text>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:strip-space elements="ENTITY"/>
+
+<xsl:template match="/">
+ <html xmlns="http://www.w3.org/1999/xhtml"><head>
+ <meta http-equiv="Content-Language" content="en-us"/>
+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
+ <meta http-equiv="Content-Style-Type" content="text/css"/>
+ <meta name="author" content="Ferruccio Guidi"/>
+ <meta name="description" content="lambda_delta digital library"/>
+ <title>lambda_delta digital library (LDDL)</title>
+ <link rel="stylesheet" type="text/css"
+ href="http://lambda-delta.info/css/ld.css"
+ />
+ <link rel="stylesheet" type="text/css"
+ href="http://lambda-delta.info/css/lddl.css"
+ />
+ <link rel="shortcut icon"
+ href="http://lambda-delta.info/download/crux_16.ico"
+ />
+ </head><body>
+ <div class="spacer">
+ <a href="http://lambda-delta.info/">
+ <img class="icon32"
+ alt="[lambda_delta home]" title="lambda_delta home"
+ src="http://lambda-delta.info/download/crux_32.png"
+ /></a>
+ </div>
+ <div class="head1">
+ <xsl:call-template name="lddl"/>
+ </div>
+ <div class="spacer">
+ <img class="rule"
+ alt="[Spacer]" title="lambda_delta rainbow rule"
+ src="http://lambda-delta.info/download/rainbow.png"
+ />
+ </div>
+ <xsl:apply-templates/>
+ <div class="spacer">
+ <a href="http://validator.w3.org/check?uri=referer">
+ <img class="w3c"
+ alt="[Valid XHTML 1.1]"
+ title="Valid XHTML 1.1"
+ src="http://www.w3.org/Icons/valid-xhtml11-blue"
+ /></a>
+ <a href="http://jigsaw.w3.org/css-validator/check/referer">
+ <img class="w3c"
+ alt="[Valid CSS level 2]"
+ title="Valid CSS level 2"
+ src="http://www.w3.org/Icons/valid-css2-blue"
+ /></a>
+ <a href="http://www.w3.org/XML/">
+ <img class="w3c"
+ alt="[Generated from XML via XSL]"
+ title="Generated from XML via XSL"
+ src="http://lambda-delta.info/download/xml_xsl2.png"
+ /></a>
+ <a href="http://lambda-delta.info/implementation.html#helena">
+ <img class="w3c"
+ alt="[Powered by Helena lambda_delta processor]"
+ title="Powered by Helena lambda_delta processor"
+ src="http://lambda-delta.info/download/helena_label.png"
+ /></a>
+ <a href="http://www.w3.org/Graphics/PNG/">
+ <img class="w3c"
+ alt="[PNG used here]"
+ title="PNG used here"
+ src="http://lambda-delta.info/download/PNGnow2.png"
+ /></a>
+ <a href="http://www.anybrowser.org/campaign/">
+ <img class="w3c"
+ alt="[Viewable with any browser]"
+ title="Viewable with any browser"
+ src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"
+ /></a>
+ </div>
+ </body></html>
+</xsl:template>
+
+<xsl:template match="ENTITY">
+ <xsl:apply-templates/>
+ <div class="text">
+ <xsl:call-template name="vpars"/>
+ <xsl:call-template name="shier"/>
+ <xsl:call-template name="qt"/>
+ <xsl:value-of select="@hierarchy"/>
+ <xsl:call-template name="qt"/>
+ <xsl:call-template name="cm"/>
+ <xsl:call-template name="sp"/>
+ <xsl:call-template name="kopts"/>
+ <xsl:call-template name="qt"/>
+ <xsl:value-of select="@options"/>
+ <xsl:call-template name="qt"/>
+ </div>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:strip-space elements="Sort LRef GRef Cast Appl Abst Abbr Void"/>
+
+<xsl:template name="separator">
+ <span class="separator">
+ <xsl:call-template name="fs"/>
+ </span>
+</xsl:template>
+
+<xsl:template match="Sort">
+ <span class="sort">
+ <xsl:call-template name="position"/>
+ </span>
+</xsl:template>
+
+<xsl:template match="LRef">
+ <span class="lref">
+ <xsl:call-template name="position"/>
+ </span>
+</xsl:template>
+
+<xsl:template match="GRef">
+ <span class="gref">
+ <xsl:call-template name="uri"/>
+ </span>
+</xsl:template>
+
+<xsl:template match="Cast">
+ <span class="cast">
+ <xsl:call-template name="oa"/>
+ <xsl:apply-templates/>
+ <xsl:call-template name="ca"/>
+ </span>
+ <xsl:call-template name="separator"/>
+</xsl:template>
+
+<xsl:template match="Appl">
+ <span class="appl">
+ <xsl:call-template name="op"/>
+ <xsl:call-template name="mk_terms"/>
+ <xsl:call-template name="cp"/>
+ </span>
+ <xsl:call-template name="separator"/>
+</xsl:template>
+
+<xsl:template match="Abst">
+ <span class="local">
+ <xsl:call-template name="lambda"/>
+ <xsl:call-template name="mk_binder">
+ <xsl:with-param name="sep-seq">
+ <xsl:call-template name="cn"/>
+ </xsl:with-param>
+ </xsl:call-template>
+ </span>
+ <xsl:call-template name="separator"/>
+</xsl:template>
+
+<xsl:template match="Abbr">
+ <span class="local">
+ <xsl:call-template name="delta"/>
+ <xsl:call-template name="mk_binder">
+ <xsl:with-param name="sep-seq">
+ <xsl:call-template name="eq"/>
+ </xsl:with-param>
+ </xsl:call-template>
+ </span>
+ <xsl:call-template name="separator"/>
+</xsl:template>
+
+<xsl:template match="Void">
+ <span class="local">
+ <xsl:call-template name="chi"/>
+ <xsl:call-template name="ob"/>
+ <xsl:call-template name="mk_names"/>
+ <xsl:call-template name="cb"/>
+ </span>
+ <xsl:call-template name="separator"/>
+</xsl:template>
+
+</xsl:stylesheet>
projects / helm.git / commitdiff