[isabelle-dev] Enabling reports in proof general
makarius at sketis.net
Thu Dec 6 16:46:17 CET 2012
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?
Posting on isabelle-dev implicitly means that you are following the
repository, and are somehow concerning about what is going on between the
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.
More information about the isabelle-dev