[isabelle-dev] Enabling reports in proof general

[Makarius]

On Tue, 4 Dec 2012, Tran Ngoc Ma wrote:

> 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?

Meta preamble:

Posting on isabelle-dev implicitly means that you are following the 
repository, and are somehow concerning about what is going on between the 
releases.

Is this the case or are you targeting add-on tools for Isabelle for 
official Isabelle2012 right now?  In that case you miss an opportunity to 
reach more people on isabelle-users who might be still interested in doing 
something with or for Proof General.  I am not doing anything against it, 
but the last time did something for it was in October 2011.


Back to your question and the official Isabelle2012 sources:
src/Pure/ProofGeneral/proof_general_emacs.ML does most of the wiring or 
that particular front-end.  There you see this:

   Output.Private_Hooks.report_fn := (fn _ => ());

It means the Prover IDE markup is ignored.  This is done because the 
feeble Elisp engine cannot easily handle what the prover emits on that 
channel.  You can try yourself to find ways to handle that voluminous 
stream, or do some filtering before sending stuff to the front-end.  The 
render_trees function in the same file already ignores quite a lot of 
markup that is part of the regular messages on the writeln/warning/error 
channels to give Proof General a chance to display it.

BTW, in 2007/2008 I spent a long time considering technical platform 
side-conditions, and resolved that JVM/Scala is strong enough to carry the 
anticipated PIDE document model of that time, but not Emacs Lisp.  I am 
still open to surprises, though.


 	Makarius