Reimplement "Decompose Proof"

[muenchnerkindl]

The Toolbox offers a "Decompose Proof" command that is handy for generating a skeleton proof following a syntactic decomposition of the hypotheses or the conclusion of the current proof obligation. Unfortunately, the Java implementation of the command is tied to the Toolbox and is therefore not available to users of the VSCode extension or other IDEs.

It would be useful to design a protocol that allows a user to interactively refine the proof obligation in the desired manner and implement it as a standalone command that can be invoked independently of any specific IDE.

[kape1395]

My plan was to use the LSP code actions to propose the user's step decomposition alternatives.