hol-mode: add hol-print-info

I recently have the problem on various machines, that have multiple
copies of HOL installed, to figure out which version is started by hol-
mode. I did this by looking at the value of HOLDIR, the current load
paths etc in ML and the used hol and holmake executables in Lisp. To
simplify this process of looking up these values, this commit adds this
functionality to hol-mode.

Remove trailing whitespace in source files.

added support for Sanity

Changed hol-mode.src and src/parse/PPBackEnd.sml so that type variables are displayed in purple.

"Everybody's cute... Everybody's cute, even me. But in purple, I'm STUNNING!"
(Centauri Ambassador Londo Molari, Babylon 5, The Parliament of Dreams)

Magnus and I removed the output filter from the emacs HOL-mode. The output filter was making printing slow.

Also, we added some ML code that will make the auto-load feature not attempt to load standard structures that are already by default loaded, e.g. String, TextIO etc.

Magnus and I added the possibility to throw away all HOL-output (including errors and warnings) inside emacs. This may sound dangerous and useless, since quitedec/interactive turns off all output except warnings and errors. However, it is useful internally sometimes. For example we hide the installation of some auxiliary ml-functions at startup using this method.

Nevertheless, a menu-entry was added to send a region to HOL and ignore all output. For completeness, a command was added as well, that toggles quitedec, sends the region and the toggles it back. Both commands might be useful when opening theories or libraries. The second one usually sends the region and just shows warnings and errors. Depending on the library / theory one is loading there might be a lot of warnings (incomplete pattern matching, free type variables etc). The first command ignores these warnings/errors as well.

A function was added to easily get information about the type of a term. Now by pressing M-h i one gets typing information about a marked term
- without context
- in the context of the surrounding term and
- in the context of the current goal.