--- a/Admin/website/TODO Tue Jun 28 11:55:30 2005 +0200
+++ b/Admin/website/TODO Tue Jun 28 11:55:30 2005 +0200
@@ -1,6 +1,11 @@
For the next release:
-- use "//" paths for alle internal static resources, due to link consistency
+- use "//" paths for alle internal static resources, due to link consistency (check it)
+
+- Spam-Schutz!? (check it)
+
+- attempt to introduce a notion of mirrors, in order to clarify
+ the relationship between main and dist
- centralize scattered project partners informations at "community"
@@ -10,14 +15,11 @@
- add CONTRIBUTORS and COPYRIGHT to Packages
-- attempt to include a notion of mirrors, in order to re-clarify
- the relationship between main and dist
-
In the mid-time:
- clarify relationship of "overview" and "logics":
- * overview: Isabelle/HOL
- * logics: Isabelle system
+ * overview: Isabelle/HOL
+ * logics: Isabelle system
Visionary:
--- a/Admin/website/build/main.mak Tue Jun 28 11:55:30 2005 +0200
+++ b/Admin/website/build/main.mak Tue Jun 28 11:55:30 2005 +0200
@@ -106,7 +106,7 @@
echo "$$outputfile: $$html"' $$(DEP_HTML)' >> $(DEP_FILE); \
echo " mkdir -p $$outputdir" >> $(DEP_FILE); \
echo " -chmod $(TARGET_UMASK_DIR) $$outputdir" >> $(DEP_FILE); \
- echo ' $(PYTHON) build/pypager.py --dtd="dtd/" $(FORCE_ENC_CMD) --srcroot="." --dstroot="$(OUTPUTROOT)" distname="$(DISTNAME)" $$< $$@' >> $(DEP_FILE); \
+ echo ' $(PYTHON) build/pypager.py --dtd="dtd/" $(FORCE_ENC_CMD) --srcroot="." --dstroot="$(OUTPUTROOT)" --spamprotect distname="$(DISTNAME)" $$< $$@' >> $(DEP_FILE); \
echo ' -$(TIDYCMD) $$@' >> $(DEP_FILE); \
echo ' chmod $(TARGET_UMASK_FILE) $$@' >> $(DEP_FILE); \
allhtml="$$allhtml$$outputfile "; \
--- a/Admin/website/build/pypager.py Tue Jun 28 11:55:30 2005 +0200
+++ b/Admin/website/build/pypager.py Tue Jun 28 11:55:30 2005 +0200
@@ -332,14 +332,14 @@
for tagname, attrname in ((u"a", u"href"), (u"img", u"src"), (u"link", u"href")):
if name == tagname:
attrs = self.transformAbsPath(attrs, attrname)
- if self.spamprotect and name = u"a":
+ if self._spamprotect and name == u"a":
value = attrs.get(u"href")
if value and value.startswith(u"mailto:"):
attrs = dict(attrs)
attrs[u"href"] = "".join([ ("&#%i;" % ord(c)) for c in value ])
for (key, value) in attrs.items():
self._out.write(u' %s=%s' % (key, quoteattr(value)))
- self._currentXPath.append(key)
+ self._currentXPath.append(name)
self._lastStart = True
def endElement(self, name):
@@ -453,7 +453,7 @@
action="store", dest="encodinghtml",
type="string", default="",
help="force value of html content encoding meta tag", metavar='encoding')
- cmdlineparser.add_option("-s", "--spamprotect",
+ cmdlineparser.add_option("-p", "--spamprotect",
action="store_true", dest="spamprotect",
help="rewrite mailto-links using entities")
--- a/Admin/website/dist/css/isabelle_print.css Tue Jun 28 11:55:30 2005 +0200
+++ b/Admin/website/dist/css/isabelle_print.css Tue Jun 28 11:55:30 2005 +0200
@@ -67,3 +67,8 @@
clear: both;
border-top: 2px solid #000000;
}
+
+/* mirrorlist */
+div.mirrorlist {
+ display: none;
+}
\ No newline at end of file
--- a/Admin/website/dist/css/isabelle_screen.css Tue Jun 28 11:55:30 2005 +0200
+++ b/Admin/website/dist/css/isabelle_screen.css Tue Jun 28 11:55:30 2005 +0200
@@ -114,23 +114,34 @@
/* mirror switch layout */
div.mirrorlist {
- margin: 2pt;
- padding: 1pt;
+ margin: 10pt;
+ padding: 0pt;
+ position: relative;
+ float: right;
+ top: 0px;
+ right: 0px;
border: 2pt solid #000000;
background-color: #EEEEDD;
+ text-align: left;
}
-div.mirrorlist h2 {
- margin: 0pt;
- padding: 2pt;
+div.mirrorlist p {
+ margin: 1pt;
+ padding: 1pt;
border: none;
background-color: #000000;
color: #EEEEDD;
- font-size: 10pt;
+ font-size: 9pt;
text-align: left;
}
div.mirrorlist ul {
- font-size: 10pt;
+ margin: 1pt 1pt 1pt 1em;
+ margin-left: 1em;
+ padding: 0pt;
+}
+
+div.mirrorlist ul li {
+ font-size: 8pt;
font-style: italics;
}
\ No newline at end of file
--- a/Admin/website/index.html Tue Jun 28 11:55:30 2005 +0200
+++ b/Admin/website/index.html Tue Jun 28 11:55:30 2005 +0200
@@ -96,7 +96,7 @@
sub/superscripts allowed in identifiers.</li>
</ul>
-<p><a href="dist/packages/Isabelle/NEWS">[Complete Changelog]</a></p>
+<p><a href="//dist/packages/Isabelle/NEWS">[Complete Changelog]</a></p>
<h2>Download</h2>
@@ -104,7 +104,7 @@
The Isabelle distribution is available
from several <a href="dist/index.html">mirror sites</a>. It includes
source and binary packages and browsable documentation. You can also
-browse the <a href="library/index.html">Isabelle theory library</a>
+browse the <a href="//library/index.html">Isabelle theory library</a>
online.
</p>
--- a/Admin/website/logics.html Tue Jun 28 11:55:30 2005 +0200
+++ b/Admin/website/logics.html Tue Jun 28 11:55:30 2005 +0200
@@ -27,7 +27,7 @@
"library/index.html">Isabelle theory library</a>).</p>
<dl>
- <dt id="isabelle_hol"><a href="library/HOL/index.html">Isabelle/HOL</a></dt>
+ <dt id="isabelle_hol"><a href="//library/HOL/index.html">Isabelle/HOL</a></dt>
<dd>is a version of classical higher-order logic resembling that of the
<a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>. The
main libraries of the HOL 4 System are now <a href=
@@ -38,11 +38,11 @@
<dd>adds Scott's Logic for Computable Functions (domain theory) to
HOL.</dd>
- <dt><a href="library/FOL/index.html">Isabelle/FOL</a></dt>
+ <dt><a href="//library/FOL/index.html">Isabelle/FOL</a></dt>
<dd>provides basic classical and intuitionistic first-order logic. It is
polymorphic.</dd>
- <dt><a href="library/ZF/index.html">Isabelle/ZF</a></dt>
+ <dt><a href="//library/ZF/index.html">Isabelle/ZF</a></dt>
<dd>offers a formulation of Zermelo-Fraenkel set theory on top of FOL.</dd>
</dl>
@@ -51,8 +51,8 @@
advanced definitional concepts like (co-)inductive sets and types,
well-founded recursion etc. The distribution also includes some large
applications, for example correctness proofs of cryptographic protocols
- (<a href="library/HOL/Auth/index.html">HOL/Auth</a>) or communication
- protocols (<a href="library/HOLCF/IOA/index.html">HOLCF/IOA</a>).</p>
+ (<a href="//library/HOL/Auth/index.html">HOL/Auth</a>) or communication
+ protocols (<a href="//library/HOLCF/IOA/index.html">HOLCF/IOA</a>).</p>
<p><em>Isabelle/ZF</em> provides another starting point for applications, with a
slightly less developed library. Its definitional packages are similar to
@@ -60,11 +60,11 @@
sets than simply-typed HOL.</p>
<p>There are a few minor object logics that may serve as further examples:
- <a href="library/CTT/index.html">CTT</a> is an extensional version of
- Martin-Löf's Type Theory, <a href="library/Cube/index.html">Cube</a> is
+ <a href="//library/CTT/index.html">CTT</a> is an extensional version of
+ Martin-Löf's Type Theory, <a href="//library/Cube/index.html">Cube</a> is
Barendregt's Lambda Cube. There are also some sequent calculus examples under
- <a href="library/Sequents/index.html">Sequents</a>, including modal and
- linear logics. Again see the <a href="library/index.html">Isabelle theory
+ <a href="//library/Sequents/index.html">Sequents</a>, including modal and
+ linear logics. Again see the <a href="//library/index.html">Isabelle theory
library</a> for other examples.</p>
<h2>Defining Logics</h2>