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?


        Makarius

_______________________________________________
ProofGeneral mailing list
ProofGeneral@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral

Reply via email to