[MLton] htmldoc pdf MLton guide

Stephen Weeks MLton@mlton.org
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
few notes.

 * 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
   the end. 

 * 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
   my machine.

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