Decide what to do with ProverStandalone

[David Aspinall <da+pgtrac@…>]

Should this code be retained or discarded? Not clear how it fits into future development plans, and already changes elsewhere in code have likely broken it. One possibility may be to move it to another plugin.

In the longer term, we've talked about adding an API to the Broker to manage running provers, so the code here would form a basis for that.

[alex heneveld]

will repair for now, unless too difficult.

used for programmatic/headless control of theorem prover -- idea is a superclass of SessionManager? which is not tied to a document (and so does not have Eclipse dependencies). no conflict with any dev plans, just good modular design i think. though there are sure to be ways it can be improved as the broker evolves.

i expect it will be essential for good unit testing (many things can be tested with a prover but without opening a document or even a workbench, therefore they should be tested without opening a document or a workbench)

also it allows third-party tools to use provers from java in more flexible ways. e.g. testing different java-based proof automation strategies (i do this with my feature wizard, trying different features or mappings to see which gives best result), or a hypothetical plugin which analyses your java code using isabelle.

[David Aspinall]

Milestone PG-Eclipse-1.0.7 deleted