HOL output has a lot of math symbols, which are encoded in Unicode. Displaying these math symbols in DOS when running HOL in Windows is not satisfying. To solve this problem, I developed a simple Java server that talks to HOL in the background, and I can use the web-browser to talk to the server. With such a system I can easily get the math symbols in the browser, and also enhance the display of HOL input/output with colors.
The code for my little work is in https://bitbucket.org/jhlchan/shell.
This is also my first experience with Bitbucket, a free source code hosting based on Mercurial, a distributed version control system. There is a nice short tutorial by Joel Spolsky, which explains clearly and simply how to use Mercurial.