--- a/Admin/website/TODO Wed May 03 17:41:28 2006 +0200
+++ b/Admin/website/TODO Thu May 04 10:13:55 2006 +0200
@@ -10,3 +10,6 @@
* overview: Isabelle/HOL
* logics: Isabelle system
(to discuss)
+
+- world_map: automated generation from coordinate data
+- world_map: more content in HTML, less in java script
\ No newline at end of file
--- a/Admin/website/build/make_dep.bash Wed May 03 17:41:28 2006 +0200
+++ b/Admin/website/build/make_dep.bash Thu May 04 10:13:55 2006 +0200
@@ -46,6 +46,7 @@
echo ' -chgrp $(TARGET_GROUP) $(dir $@)' >> "$DEP_FILE"
echo ' -[ -e $@ ] && rm $@' >> "$DEP_FILE"
echo ' $(PYTHON) build/pypager.py --dtd="dtd/" $(FORCE_ENC_CMD) --srcroot="." --dstroot="$(OUTPUTROOT)" distname="$(DISTNAME)" $< $@' >> "$DEP_FILE"
+ echo ' $(PYTHON) build/obfusmail.py --dtd="dtd/" $@' >> "$DEP_FILE"
echo ' -$(TIDYCMD) $@' >> "$DEP_FILE"
echo ' chmod $(TARGET_UMASK_FILE) $@' >> "$DEP_FILE"
echo ' chgrp $(TARGET_GROUP) $@' >> "$DEP_FILE"
@@ -55,5 +56,4 @@
echo "DEP_ALLHTML=$allhtml" >> "$DEP_FILE"
echo >> "$DEP_FILE"
echo 'allsite: $(DEP_ALLHTML) $(DEP_ALLSTATIC)' >> "$DEP_FILE"
-echo ' $(PYTHON) build/obfusmail.py --dtd="dtd/"' "$allhtml" >> "$DEP_FILE"
echo ".PHONY: allsite" >> "$DEP_FILE"
--- a/Admin/website/build/obfusmail.py Wed May 03 17:41:28 2006 +0200
+++ b/Admin/website/build/obfusmail.py Thu May 04 10:13:55 2006 +0200
@@ -43,12 +43,11 @@
pass
- def __init__(self, dtd, filename, mails, encs):
+ def __init__(self, dtd, mails, enc):
super(FindHandler, self).__init__(self.DevZero(), 'UTF-8', dtd)
- self.filename = filename
self.mails = mails
- self.encs = encs
+ self.enc = enc
self.pending_mail = None
def startElement(self, name, attrs):
@@ -61,7 +60,7 @@
if name == u'meta' and attrs.get(u'http-equiv', u'').lower() == u'content-type':
content = attrs.get(u'content', u'')
if content.startswith(u'text/html; charset='):
- self.encs[self.filename] = content[19:]
+ self.enc = content[19:]
def endElement(self, name):
@@ -69,8 +68,8 @@
if self.pending_mail is not None:
baremail = "%s@%s" % split_mail(self.pending_mail)[0]
if self.currentContent() != baremail:
- raise Exception("In '%s', inconsistent mail address: '%s' vs. '%s'" % (self.filename, self.currentContent(), baremail))
- self.mails[(self.filename, self.pending_mail)] = True
+ raise Exception("Inconsistent mail address: '%s' vs. '%s'" % (self.currentContent(), baremail))
+ self.mails[self.pending_mail] = True
self.pending_mail = None
super(FindHandler, self).endElement(name)
@@ -80,10 +79,9 @@
class ReplaceHandler(TransformerHandler):
- def __init__(self, out, dtd, filename, encoding, mails):
+ def __init__(self, out, dtd, encoding, mails):
super(ReplaceHandler, self).__init__(out, encoding, dtd)
- self.filename = filename
self.pending_mail = None
self.mails = mails
@@ -102,7 +100,7 @@
if name == u'a':
if self.pending_mail is not None:
self.flushCharacterBuffer()
- self._out.write(self.mails[(self.filename, self.pending_mail)])
+ self._out.write(self.mails[self.pending_mail])
self.pending_mail = None
return
@@ -148,7 +146,7 @@
# parse command line
cmdlineparser = optparse.OptionParser(
- usage = '%prog [options] htmlfiles*',
+ usage = '%prog [options] htmlfile',
conflict_handler = "error",
description = '''Protecting mail adresses in html files by obfuscating''',
add_help_option = True,
@@ -158,30 +156,28 @@
type="string", default=".",
help="local mirror of XHTML DTDs", metavar='location')
- options, filenames = cmdlineparser.parse_args(sys.argv[1:])
+ options, (filename,) = cmdlineparser.parse_args(sys.argv[1:])
# find mails
mails = {}
- encs = {}
- for filename in filenames:
- istream = open(filename, 'r')
- findhandler = FindHandler(options.dtd, filename, mails, encs)
- parseWithER(istream, findhandler)
- istream.close()
+ enc = outputEncoding
+ istream = open(filename, 'r')
+ findhandler = FindHandler(options.dtd, mails, enc)
+ parseWithER(istream, findhandler)
+ enc = findhandler.enc
+ istream.close()
- # transform mails
- mails_subst = {}
- filenames = {}
- for filename, mail in mails.iterkeys():
- filenames[filename] = True
- mails_subst[(filename, mail)] = obfuscate(mail, filename)
-
- # transform pages
- for filename in filenames.iterkeys():
+ if mails:
+ # transform mails
+ mails_subst = {}
+ for mail in mails.iterkeys():
+ mails_subst[mail] = obfuscate(mail, filename)
+
+ # transform pages
istream = StringIO(open(filename, 'r').read())
ostream = open(filename, 'wb')
- print "writing %s with %s" % (filename, encs.get(filename, outputEncoding))
- replacehandler = ReplaceHandler(ostream, options.dtd, filename, encs.get(filename, outputEncoding), mails_subst)
+ print "writing %s with %s" % (filename, enc)
+ replacehandler = ReplaceHandler(ostream, options.dtd, enc, mails_subst)
parseWithER(istream, replacehandler)
ostream.close()
istream.close()
--- a/Admin/website/include/htmlheader.include.html Wed May 03 17:41:28 2006 +0200
+++ b/Admin/website/include/htmlheader.include.html Thu May 04 10:13:55 2006 +0200
@@ -5,7 +5,7 @@
<?contentType?>
<!-- the very base - here all elements are fixed to a certain base style -->
<link rel="stylesheet" type="text/css" media="all" href="//css/aelfwine.css"/>
- <!-- basic isabelle-site-specific styles -->
+ <!-- basic isabelle site-specific styles -->
<link rel="stylesheet" type="text/css" media="all" href="//css/isabelle_base.css"/>
<!-- advanced sceen styles - they are imported such that they are ignored by old-fashioned browsers -->
<style type="text/css" media="screen">
@@ -16,5 +16,5 @@
<link rel="icon" href="//img/favicon.ico" type="image/icon"/>
<meta name="language" content="en"/>
<meta name="robots" content="index follow"/>
- <meta name="author" content="Tobias Nipkow, Lawrence Paulson, Markus Wenzel, Gerwin Klein, Florian Haftmann" />
+ <meta name="author" content="Tobias Nipkow, Lawrence Paulson, Markus Wenzel, Gerwin Klein, Florian Haftmann, Tjark Weber" />
</dummy:wrapper>
\ No newline at end of file
--- a/Admin/website/overview.html Wed May 03 17:41:28 2006 +0200
+++ b/Admin/website/overview.html Thu May 04 10:13:55 2006 +0200
@@ -4,12 +4,95 @@
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
- <title>World map</title>
+ <title>Overview</title>
<?include file="//include/htmlheader.include.html"?>
</head>
<body class="main">
+ <?include file="//include/header.include.html"?>
+ <div class="hr"><hr/></div>
+ <?include file="//include/navigation.include.html"?>
+ <div class="hr"><hr/></div>
+ <div id="content">
+
+ <h2>What is Isabelle?</h2>
+ <p>
+ Isabelle is a generic proof assistant. It allows mathematical
+ formulas to be expressed in a formal language and provides tools
+ for proving those formulas in a logical calculus. The main
+ application is the formalization of mathematical proofs and in
+ particular <em>formal verification</em>, which includes proving
+ the correctness of computer hardware or software and proving
+ properties of computer languages and protocols.</p>
+ <p>Compared with similar tools, Isabelle's distinguishing feature is its
+ flexibility. Most proof assistants are built around a single formal calculus,
+ typically higher-order logic. Isabelle has the capacity to accept a variety
+ of formal calculi. The distributed version supports higher-order logic but
+ also axiomatic set theory and several other formalisms. See
+ <a href="logics.html">logics</a> for more details.</p>
+
+ <p>Isabelle is a joint project between Lawrence C. Paulson
+ (University of Cambridge, UK) and Tobias Nipkow (Technical
+ University of Munich, Germany).</p>
+
+ <p>Isabelle is distributed <em>freely</em> as Open Source
+ Software <!--a href="//dist/Isabelle/COPYRIGHT"-->BSD
+ license<!--/a-->; see the <a
+ href="installation.html">installation instructions</a>.</p>
+
+ <h2>Preview of Isabelle</h2>
+
+ <a href="//media/pg_preview.mov">
+ <img class="left" src="//img/screenshot_isabelle_pg.png" alt="Isabelle Screenshot"
+ width="250" height="277" />
+ </a>
+
+ <p>Here is a <a href="//media/pg_preview.mov">hyperlinked preview</a> demonstrating
+ Isabelle and ProofGeneral, in <a href="http://www.apple.com/quicktime/download/">QuickTime
+ format</a> and in <a href="//media/pg_preview.pdf">PDF</a>.</p>
+ <br clear="all"/>
+
+ <h2>What Isabelle offers</h2>
+
+ <p>Isabelle provides excellent notational support: new notations
+ can be introduced, using normal mathematical symbols. Proofs can
+ be written in a structured notation based upon traditional proof
+ style, or more straightforwardly as sequences of
+ commands. Definitions and proofs may include TeX source, from
+ which Isabelle can automatically generate typeset documents.</p>
+
+ <p>The main limitation of all such proof systems is that proving
+ theorems requires much effort from an expert user. Isabelle
+ incorporates some tools to improve the user's productivity by
+ automating some parts of the proof process. In particular,
+ Isabelle's <em>classical reasoner</em> can perform long chains
+ of reasoning steps to prove formulas. The <em>simplifier</em>
+ can reason with and about equations. Linear <em>arithmetic</em>
+ facts are proved automatically.</p>
+
+ <p>Isabelle comes with a large theory library of formally
+ verified mathematics, including elementary number theory (for
+ example, Gauss's law of quadratic reciprocity), analysis (basic
+ properties of limits, derivatives and integrals), algebra (up to
+ Sylow's theorem) and set theory (the relative consistency of the
+ Axiom of Choice). Also provided are numerous examples arising
+ from research into formal verification.</p>
+
+ <p>With <em>Isar</em>, Isabelle offers a concise proof formulation language
+ which enables a user to write proof scripts naturally understandable for
+ both humans <em>and</em> computers.</p>
+
+ <p>Isabelle is closely integrated with the <a href=
+ "http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> user interface, which
+ eases the task of writing and maintaining proof scripts.</p>
+
+ <p>Ample <a href="documentation.html">documentation</a> is available
+ about using Isabelle and its inner concepts, including a
+ <a href="http://www4.in.tum.de/~nipkow/LNCS2283/">Tutorial</a> published by
+ Springer-Verlag.</p>
+
+ </div>
<div class="hr"><hr/></div>
<?include file="//include/footer.include.html"?>
</body>