Extract Isabelle-specific behaviour; design prover extension point

[David Aspinall <da+pgtrac@…>]

We should extract the Isabelle specific behaviour of the current plugin, and implement it as a prover extension. This will give a much better handle to people who want to connect new provers.

The risk here is that we are recovering the existing Proof General Emacs architecture, and end up with lots of prover-specific code which circumvents PGIP. However, using prover-specific enhancements may be a good way to evolve PGIP, just as Proof General evolved (product-line architecture). Another problem is that extension point connections are mainly static, whereas PGIP supports some dynamic configuration and connection/discovery of provers via the Broker and <proverconfig> messages. In practice it seems unlikely that this will be used much, and it is possible that we could use the <proverconfig> messages themselves to generate a plugin declaration dynamically (or perhaps, using a tool to generate an initial plugin project).

[David Aspinall]

Milestone PG-Eclipse-1.1.0 deleted