Fix bug in Moscow ML version of LaTeX munger

Issue was that Moscow ML mungers start by executing the SML code in the
various theories that are built into them. This can cause warning
messages, and these warnings were written to standard out. This then
causes the output to be other than desired. (Standard out should only
contain the munged LaTeX source.)

There's code that runs before the lexing loop starts to switch HOL
warnings to standard error, but this is executed after the theories
load. So, yes, it would be nice if theory structures were side-effect
free, but we actually want theories to induce all sorts of side effects
as they load, and thus code needs to execute, and that code might cause
messages to go to standard out.

By contrast, in Poly/ML things are staged: the theories are loaded once
and put into the heap that is then executed to implement the munger's
lexing. This makes things more efficient of course, and also means that
warnings on theory loads are emitted when the munger is built, not when
it is run.

The fix in the Moscow ML world is to make the final munger executable
include an object file (warning_stream.uo) that sets the warning stream
appropriately. Because Moscow ML loads things in the order they appear
on the compilation command-line (to the extent that this is possible),
this is executed before the theories are executed, and all is well.

trailing newlines in *.{sml,sig} files from src/ removed

Trailing newlines from SML files in src/ were rendered in HTML documentation.

Make staticness of munger optional, and not the default.

(On my installation of MacOS (10.5.8), static mungers fail to build.
On Linux, it works but creates piles of awful warnings about symbols.)

mkmunge can now take a -o filename option to specify name of resulting munger.

TeX mkmunge now builds with Moscow ML; Poly version calls C compiler too.