doc: Predump format for faster TeXing.