Unix, HTML, and the LaTeX computer typography system