some minor improvements
authorhaftmann
Tue, 28 Jun 2005 12:03:43 +0200
changeset 16579 094a538d8813
parent 16578 b434de794092
child 16580 510b5fc86bf4
some minor improvements
Admin/website/build/main.mak
Admin/website/build/pypager.py
Admin/website/include/mirrorlist.major.include.html
Admin/website/include/mirrorlist.minor.include.html
--- a/Admin/website/build/main.mak	Tue Jun 28 12:03:19 2005 +0200
+++ b/Admin/website/build/main.mak	Tue Jun 28 12:03:43 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)" --spamprotect distname="$(DISTNAME)" $$< $$@' >> $(DEP_FILE); \
+		echo '	$(PYTHON) build/pypager.py --dtd="dtd/" $(FORCE_ENC_CMD) --srcroot="." --dstroot="$(OUTPUTROOT)" 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 12:03:19 2005 +0200
+++ b/Admin/website/build/pypager.py	Tue Jun 28 12:03:43 2005 +0200
@@ -257,7 +257,7 @@
 # the XML transformer
 class TransformerHandler(ContentHandler, EntityResolver):
 
-    def __init__(self, out, encoding, dtd, func, spamprotect):
+    def __init__(self, out, encoding, dtd, func):
 
         ContentHandler.__init__(self)
         #~ EntityResolver.__init__(self)
@@ -268,7 +268,6 @@
         self._encoding = encoding
         self._lastStart = False
         self._func = func
-        self._spamprotect = spamprotect
         self._characterBuffer = {}
         self._currentXPath = []
         self._title = None
@@ -284,8 +283,6 @@
     def flushCharacterBuffer(self):
 
         content = escape(u"".join(self._characterBuffer))
-        if self._currentXPath and self._currentXPath[-1] == u"a":
-            content = content.replace(u"@", u"&#64;")
         self._out.write(content)
         self._characterBuffer = []
 
@@ -335,11 +332,6 @@
         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":
-            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(name)
@@ -456,9 +448,6 @@
         action="store", dest="encodinghtml",
         type="string", default="",
         help="force value of html content encoding meta tag", metavar='encoding')
-    cmdlineparser.add_option("-p", "--spamprotect",
-        action="store_true", dest="spamprotect",
-        help="rewrite mailto-links using entities")
 
     options, args = cmdlineparser.parse_args(sys.argv[1:])
 
@@ -501,7 +490,7 @@
         ostream = sys.stdout
 
     # process file
-    transformer = TransformerHandler(ostream, outputEncoding, options.dtd, func, options.spamprotect)
+    transformer = TransformerHandler(ostream, outputEncoding, options.dtd, func)
     parseWithER(istream, transformer)
 
     # close handles
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/include/mirrorlist.major.include.html	Tue Jun 28 12:03:43 2005 +0200
@@ -0,0 +1,10 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE div PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<!-- $Id$ -->
+<div class="mirrorlist">
+    <h2>Switch mirror:</h2>
+    <ul>
+        <?mirror prefix="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/" title="Cambridge" ?>
+        <?mirror prefix="http://isabelle.in.tum.de/"                     title="Munich"    ?>
+    </ul>
+</div>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/include/mirrorlist.minor.include.html	Tue Jun 28 12:03:43 2005 +0200
@@ -0,0 +1,11 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE div PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<!-- $Id$ -->
+<div class="mirrorlist">
+    <h2>Switch mirror:</h2>
+    <ul>
+        <li><?mirror prefix="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/" title="Cambridge (.uk)" ?></li>
+        <li><?mirror prefix="http://isabelle.in.tum.de/"                     title="Munich (.de)"    ?></li>
+        <li><?mirror prefix="http://mirror.cse.unsw.edu.au/pub/isabelle/"    title="Sydney (.au)"    ?></li>
+    </ul>
+</div>