On Thu, 16 Dec 2010, Michael Chan wrote:
Can you explain which messages are getting in the way in particular?
Mostly, the 'Unification bound exceeded' warnings. Exceeding the unification
bound is an expected behaviour in my application, so I think it should be
safe to suppress the warning at times. The main problem is that my system
pretty prints out the tenv and tyenv when it pulls matchers from a sequence
returned by Unify.matchers, but if I get a warning at a particular matcher, I
lose the buffer containing the previous output.
Did yout try the tracing channel for your messages?
ProofGeneral mailing list