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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
