This is triggered by an environment variable that points at a file that
is used to cache polling results. If the variable is not specified just
use all mirror links as usual. This way, for random builds when people
try things out there is no problem, while the nightly builds (and my
manual builds when there are changes) do the right thing.
The file holds information about the polls, and verifies that the
download exists -- if not, the link is not shown. If it is, then it
tries to get the size of the remote file (via HEAD or via FTP), and if
it doesn't match our download information, then drop it too. If no size
informaion is available, include it, but re-poll after a few days. Even
if the size matches, a re-poll will be done after a month, so stale
mirrors will not stick.
necessary modules are now "all.rkt"s; "shard.rkt"s turn to
"resources.rkt".
Also, "navbar.rkt" changes to "all.rkt", since it was doing the same
thing (in addition to setting the navbar).
Ie, the difference between using it as a language and as a module is now
the same in both. Also, improve `scribble/html' (and
`scribble/html/htmllang') by reproviding most of the corresponding text
modules.
Change `meta/web' accordingly, and improve code by making a new langugae
(`#lang meta/web'). This language is similar to `scribble/html' except
that it uses the plain scribble reader (not the `-inside' one), it
doesn't use the customized module-begin feature (that uses
`output-xml'), and it adds all the relevant bits of `meta/web/common'.
(Also, "meta/web/common.rkt" is gone, since it's used only as a language
now.)
This commit has lots of details and binding games, so it's tricky, and
potentially caused some problems. (Took me a while to track many
breakages, so I won't be surprised if there are more.)
