# HG changeset patch # User haftmann # Date 1119952530 -7200 # Node ID 15d5f8e729fe00ce3f084cf007460e0bc6528946 # Parent 57d4c33c51848a5ed00a40a2b421ae58f901d15e some minor improvements diff -r 57d4c33c5184 -r 15d5f8e729fe Admin/website/TODO --- 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: diff -r 57d4c33c5184 -r 15d5f8e729fe Admin/website/build/main.mak --- 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 "; \ diff -r 57d4c33c5184 -r 15d5f8e729fe Admin/website/build/pypager.py --- 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") diff -r 57d4c33c5184 -r 15d5f8e729fe Admin/website/dist/css/isabelle_print.css --- 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 diff -r 57d4c33c5184 -r 15d5f8e729fe Admin/website/dist/css/isabelle_screen.css --- 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 diff -r 57d4c33c5184 -r 15d5f8e729fe Admin/website/index.html --- 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. -

[Complete Changelog]

+

[Complete Changelog]

Download

@@ -104,7 +104,7 @@ The Isabelle distribution is available from several mirror sites. It includes source and binary packages and browsable documentation. You can also -browse the Isabelle theory library +browse the Isabelle theory library online.

diff -r 57d4c33c5184 -r 15d5f8e729fe Admin/website/logics.html --- 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).

-
Isabelle/HOL
+
Isabelle/HOL
is a version of classical higher-order logic resembling that of the HOL System. The main libraries of the HOL 4 System are now adds Scott's Logic for Computable Functions (domain theory) to HOL.
-
Isabelle/FOL
+
Isabelle/FOL
provides basic classical and intuitionistic first-order logic. It is polymorphic.
-
Isabelle/ZF
+
Isabelle/ZF
offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
@@ -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 - (HOL/Auth) or communication - protocols (HOLCF/IOA).

+ (HOL/Auth) or communication + protocols (HOLCF/IOA).

Isabelle/ZF 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.

There are a few minor object logics that may serve as further examples: - CTT is an extensional version of - Martin-Löf's Type Theory, Cube is + CTT is an extensional version of + Martin-Löf's Type Theory, Cube is Barendregt's Lambda Cube. There are also some sequent calculus examples under - Sequents, including modal and - linear logics. Again see the Isabelle theory + Sequents, including modal and + linear logics. Again see the Isabelle theory library for other examples.

Defining Logics