On Thu, 6 Dec 2012, Makarius wrote:
On Tue, 4 Dec 2012, Tran Ngoc Ma wrote:
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.
Reading this again, I realize that there is more to say about it.
Putting a suitable function into Output.Private_Hooks.report_fn is one
thing, but there are many more spots where the "legacy mode" of Proof
General is implicitly distinguished from the "official mode" of the
document model behind Isabelle/Scala. Position.is_reported in particular.
The presence or absence of official command transaction ids is often used
to distinguish the two worlds, the old and the new. Changing that
slightly, will cause big problems.
We are speaking about the internal protocols here, and these are "system
private" by construction. The legacy mode still happens to be there, but
conceptually it is not realistic to make add-ons on that. To participate
in the benefits of PIDE infrastructure in the proper way, you would have
to connect to the Isabelle/Scala API, as does Isabelle/jEdit already.
Isabelle/jEdit is only special in being the "flagship application" of the
Isabelle/PIDE framework -- and in living on the same Scala/JVM
environment.
A master student in Bremen has worked on another editor front-end for
Isabelle/Scala this year, targeting some web client with an editor based
on HTML technology. Hopefully the results will become publicly available
soon.
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?
This is actually very relevant for your project. If it is an experiment
on the internal protocols that implement the Scala APIs, it will depend on
the version you use. A stable release remains stable for several months.
The repository changes all the time, especially the PIDE protocol layer.
(For the coming release at the start of 2013 it should converge about
now.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
