A Texinfo-to-HTML direct translator.