Cleanup: Removal of key.api package

[wadoon]

Removal of the package key.api. This package once drove the development of the proof script debugger.

The package always lags behind its potential and is definitively not in shape or functional.

The better alternative is to use the classes directly. Or wait until the REST API arrives.

[mattulbrich]

What does it mean "use the classes directly"? Is there no functionality in this package currently needed anywhere? Is this type of Java API fully superseded by the REST-API?

[wadoon]

What does it mean "use the classes directly"? Is there no functionality in this package currently needed anywhere? Is this type of Java API fully superseded by the REST-API?

We won't have a REST-API. We are introducing a JSON-RPC. A REST-API builds upon the HTTP methods.

key.api was a wrapper for some functionalities in KeY, needed in the ProofScriptDebugger. The idea was to have a simple API. But during the development of PSDBG it arose that an API hiding the internal information is not effective for complex applications.

In the future: If you are using a JVM language (Kotlin, Clojure, ...) you should use the KeY classes directly instead of the key.api, e.g., key.api.ProofManagement vs. Proof and ProofControl. For any non-JVM language, use JSON-RPC.

The key.api has one used functionality that was missing in key.core: getting the list of all contracts. This function was moved to KeYEnvironment.

There is also the "matcher" functionality used in the PSDBG (e.g., you remember f(... ?X ...)?), but in KeY it is unused and untested. Probably it is rotted now.

[mattulbrich]

Alright. Thanks for the clarification.

The matching part may be relevant for proof scripts one day, but we can still find it in the history