[MLton] htmldoc pdf MLton guide
Tue, 15 Nov 2005 14:12:14 -0800
I took Adam's patch for using htmldoc to make a PDF version of the
MLton Guide and turned it into a separate script, bin/make-pdf-guide,
so it can be run independently of grab-wiki. make-pdf-guide runs on
the html in doc/guide and generates doc/guide/mlton-guide.pdf. I also
fixed all of the remaining problems (that I noticed anyway). Here's a
* I don't think there needs to be a table of contents, since the
index is at the front and everything is alphabetized.
* I eliminated the pictures from the html and turned them into links.
So, the file is much smaller (1.7M vs 4.4M) and there is no problem
with pictures being cutoff. Plus, one doesn't need to be online to
run make-pdf-guide. With the pictures still in, htmldoc had been
downloading the pictures from mlton.org each time it ran.
* I dropped all the font tags, which had (only) been used to set
colors for code, and were incorrectly handled by htmldoc. As a
result, the document is basically black and white, but that's fine.
I had tried htmldoc's --gray option, but it seemed to be ignored.
* I tweaked the alphabetization of pages so that the lower case
entries are mixed in with the upper case, instead of appearing at
* I tweaked the header and footer a bit.
* I eliminated some redundant HTML title stuff at the beginning of
each page, since the same information appears in the header.
* Generating the pdf guide is now extremely fast, taking 5 seconds on
All in all I think the output looks great, and should definitely go in
the release. I don't know of any other problems, but it would be
great if people could take a look at the pdf. If you have htmldoc and
SVN head, you can generate the pdf with the script. If not, I've put
the pdf at