# HG changeset patch
# User haftmann
# Date 1146670888 -7200
# Node ID bc0bef4a124e11047bf69d8d483163c232c04e26
# Parent  9d15911f18938e2213ca9bdb63f03d6df9ff8e6b
added world map

diff -r 9d15911f1893 -r bc0bef4a124e Admin/website/build/obfusmail.py
--- a/Admin/website/build/obfusmail.py	Wed May 03 12:05:53 2006 +0200
+++ b/Admin/website/build/obfusmail.py	Wed May 03 17:41:28 2006 +0200
@@ -23,6 +23,18 @@
 # global configuration
 outputEncoding = 'UTF-8'
 
+def split_mail(mail):
+
+    mail_arg = mail.split("?", 2)
+    if len(mail_arg) == 2:
+        mail, arg = mail_arg
+    else:
+        mail = mail_arg[0]
+        arg = None
+    name, host = mail.split("@", 2) 
+
+    return ((name, host), arg)
+
 class FindHandler(TransformerHandler):
 
     class DevZero(object):
@@ -31,11 +43,12 @@
 
             pass
 
-    def __init__(self, dtd, filename, mails):
+    def __init__(self, dtd, filename, mails, encs):
 
-        super(FindHandler, self).__init__(self.DevZero(), outputEncoding, dtd)
+        super(FindHandler, self).__init__(self.DevZero(), 'UTF-8', dtd)
         self.filename = filename
         self.mails = mails
+        self.encs = encs
         self.pending_mail = None
 
     def startElement(self, name, attrs):
@@ -45,13 +58,18 @@
             if href.startswith(u'mailto:'):
                 self.pending_mail = href[7:]
         super(FindHandler, self).startElement(name, attrs)
+        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:]
 
     def endElement(self, name):
 
         if name == u'a':
             if self.pending_mail is not None:
-                if self.currentContent() != self.pending_mail:
-                    raise Exception("Inconsistent mail address: '%s' vs. '%s'" % (self.currentContent(), self.pending_mail))
+                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
                 self.pending_mail = None
         super(FindHandler, self).endElement(name)
@@ -62,9 +80,9 @@
 
 class ReplaceHandler(TransformerHandler):
 
-    def __init__(self, out, dtd, filename, mails):
+    def __init__(self, out, dtd, filename, encoding, mails):
 
-        super(ReplaceHandler, self).__init__(out, outputEncoding, dtd)
+        super(ReplaceHandler, self).__init__(out, encoding, dtd)
         self.filename = filename
         self.pending_mail = None
         self.mails = mails
@@ -111,12 +129,17 @@
         if n != 0:
             raise Exception("shell cmd error: %s" % n)
 
-    name, host = mailaddr.split("@", 2)
-    imgname = (name + "_" + host).replace(".", "_"). replace("?", "_") + ".png"
+    ((name, host), arg) = split_mail(mailaddr)
+    baremail = "%s@%s" % (name, host)
+    imgname = (name + "_" + host).replace(".", "_") + ".png"
     imgfile = path.join(path.split(htmlfile)[0], imgname)
-    cmd("convert label:'%s' '%s'" % (mailaddr, imgfile))
-    mailsimple = u"{%s} AT [%s]" % (name, host)
-    mailscript = u" ".join(map(mk_line, ['<a href="', "mailto:", name, "@", host, '">']));
+    cmd("convert label:'%s' '%s'" % (baremail, imgfile))
+    if arg is not None:
+        mailsimple = u"{%s} AT [%s] WITH (%s)" % (name, host, arg)
+        mailscript = u" ".join(map(mk_line, ['<a href="', "mailto:", name, "@", host, "?", arg, '">']));
+    else:
+        mailsimple = u"{%s} AT [%s]" % (name, host)
+        mailscript = u" ".join(map(mk_line, ['<a href="', "mailto:", name, "@", host, '">']));
     mailimg = '<img src=%s style="vertical-align:middle" alt=%s />' % (quoteattr(imgname), quoteattr(mailsimple))
 
     return (mk_script(mailscript) + mailimg + mk_script(mk_line("</a>")))
@@ -139,22 +162,26 @@
 
     # find mails
     mails = {}
+    encs = {}
     for filename in filenames:
         istream = open(filename, 'r')
-        findhandler = FindHandler(options.dtd, filename, mails)
+        findhandler = FindHandler(options.dtd, filename, mails, encs)
         parseWithER(istream, findhandler)
         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:
+    for filename in filenames.iterkeys():
         istream = StringIO(open(filename, 'r').read())
         ostream = open(filename, 'wb')
-        replacehandler = ReplaceHandler(ostream, options.dtd, filename, mails_subst)
+        print "writing %s with %s" % (filename, encs.get(filename, outputEncoding))
+        replacehandler = ReplaceHandler(ostream, options.dtd, filename, encs.get(filename, outputEncoding), mails_subst)
         parseWithER(istream, replacehandler)
         ostream.close()
         istream.close()
diff -r 9d15911f1893 -r bc0bef4a124e Admin/website/build/project.mak
--- a/Admin/website/build/project.mak	Wed May 03 12:05:53 2006 +0200
+++ b/Admin/website/build/project.mak	Wed May 03 17:41:28 2006 +0200
@@ -7,7 +7,7 @@
 	@echo 'If you have no makedist at hand, check out default $@ from CVS'; \
 	@false; \
 
-STATICDIRS=css img media misc
+STATICDIRS=css img media misc js
 STATICFILES=include/documentationdist.include.html
 OUTPUTDIST_REL=dist-$(DISTNAME)
 OUTPUTDIST=$(OUTPUTROOT)/$(OUTPUTDIST_REL)
diff -r 9d15911f1893 -r bc0bef4a124e Admin/website/build/pypager.py
--- a/Admin/website/build/pypager.py	Wed May 03 12:05:53 2006 +0200
+++ b/Admin/website/build/pypager.py	Wed May 03 17:41:28 2006 +0200
@@ -273,7 +273,7 @@
         if name == u"dummy:wrapper":
             return
         # this list is not exhaustive
-        for tagname, attrname in ((u"a", u"href"), (u"img", u"src"), (u"link", u"href")):
+        for tagname, attrname in ((u"a", u"href"), (u"img", u"src"), (u"link", u"href"), (u"script", u"src")):
             if name == tagname:
                 attrs = self.transformAbsPath(attrs, attrname)
         super(FunctionsHandler, self).startElement(name, attrs)
diff -r 9d15911f1893 -r bc0bef4a124e Admin/website/community.html
--- a/Admin/website/community.html	Wed May 03 12:05:53 2006 +0200
+++ b/Admin/website/community.html	Wed May 03 17:41:28 2006 +0200
@@ -27,6 +27,10 @@
       "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/projects.html">projects</a>
       undertaken using Isabelle.</p>
 
+      <h2>Isabelle in your neighbourhood</h2>
+
+      <p>Find out on the <a href="//world_map.html">world map</a>!</p>
+
       <h2>Mailing list</h2> 
 
       <p>You may use the mailing list <a href=
@@ -34,7 +38,7 @@
           <a href="https://lists.cam.ac.uk/pipermail/cl-isabelle-users/index.html">archive</a> to discuss
           problems and results.
           To subscribe, contact our robot:
-          <a href="mailto:Cl-isabelle-users-request@lists.cam.ac.uk?subject=subscribe">Cl-isabelle-users-request@lists.cam.ac.uk?subject=subscribe</a>.
+          <a href="mailto:Cl-isabelle-users-request@lists.cam.ac.uk?subject=subscribe">Cl-isabelle-users-request@lists.cam.ac.uk</a>.
     </p>
 
       <h2>Contributing theorems</h2>
diff -r 9d15911f1893 -r bc0bef4a124e Admin/website/css/isabelle_screen.css
--- a/Admin/website/css/isabelle_screen.css	Wed May 03 12:05:53 2006 +0200
+++ b/Admin/website/css/isabelle_screen.css	Wed May 03 17:41:28 2006 +0200
@@ -134,7 +134,7 @@
 
 div.mirrorlist ul li {
     font-size: 8pt;
-    font-style: italics;
+    font-style: italic;
     padding: 0pt 12pt 0pt 0pt;
 }
 
diff -r 9d15911f1893 -r bc0bef4a124e Admin/website/documentation.html
--- a/Admin/website/documentation.html	Wed May 03 12:05:53 2006 +0200
+++ b/Admin/website/documentation.html	Wed May 03 17:41:28 2006 +0200
@@ -36,7 +36,7 @@
           <a href="https://lists.cam.ac.uk/pipermail/cl-isabelle-users/index.html">archive</a> to discuss
           problems and results.
                     To subscribe, contact our robot:
-          <a href="mailto:Cl-isabelle-users-request@lists.cam.ac.uk?subject=subscribe">Cl-isabelle-users-request@lists.cam.ac.uk?subject=subscribe</a>.
+          <a href="mailto:Cl-isabelle-users-request@lists.cam.ac.uk?subject=subscribe">Cl-isabelle-users-request@lists.cam.ac.uk</a>.
             </p>
         <p>Please consult the <a href="http://isabelle.in.tum.de/faq.html">FAQ</a> for answers to frequent
         problems.</p>
diff -r 9d15911f1893 -r bc0bef4a124e Admin/website/img/world_map.gif
Binary file Admin/website/img/world_map.gif has changed
diff -r 9d15911f1893 -r bc0bef4a124e Admin/website/img/world_map_large.gif
Binary file Admin/website/img/world_map_large.gif has changed
diff -r 9d15911f1893 -r bc0bef4a124e Admin/website/index.html
--- a/Admin/website/index.html	Wed May 03 12:05:53 2006 +0200
+++ b/Admin/website/index.html	Wed May 03 17:41:28 2006 +0200
@@ -74,7 +74,7 @@
           <a href="https://lists.cam.ac.uk/pipermail/cl-isabelle-users/index.html">archive</a> to
 discuss problems and results.
       To subscribe, contact our robot:
-      <a href="mailto:Cl-isabelle-users-request@lists.cam.ac.uk?subject=subscribe">Cl-isabelle-users-request@lists.cam.ac.uk?subject=subscribe</a>.
+      <a href="mailto:Cl-isabelle-users-request@lists.cam.ac.uk?subject=subscribe">Cl-isabelle-users-request@lists.cam.ac.uk</a>.
 </p>
 
     </div>
diff -r 9d15911f1893 -r bc0bef4a124e Admin/website/overview.html
--- a/Admin/website/overview.html	Wed May 03 12:05:53 2006 +0200
+++ b/Admin/website/overview.html	Wed May 03 17:41:28 2006 +0200
@@ -4,95 +4,12 @@
 <html xmlns="http://www.w3.org/1999/xhtml">
 
 <head>
-    <title>Overview</title>
+    <title>World map</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>