[isabelle-dev] Enabling reports in proof general

[Makarius]

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