#
f46c9c02 |
|
01-Apr-2015 |
Michael Norrish <michael.norrish@nicta.com.au> |
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.
|