[isabelle-dev] Enabling reports in proof general

Tran Ngoc Ma TranNgoc.Ma at nicta.com.au
Tue Dec 4 23:25:10 CET 2012

Hi all,

I'm working on a tool that uses prover markup to give jEdit-like information for proof general users. It basically gives what the tooltips tell you in jEdit, along with the definitions if possible.

I need to inspect and store some of the reports emitted by the prover. With jEdit, this is done simply by changing the private hooks in output; however it seems like something else needs to be done for proof general, as there doesn't appear to be any reports emitted. Am I missing something here? If not, how do I enable reporting in proof general?

Thanks heaps

Tran Ma


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

More information about the isabelle-dev mailing list