Make WD semantics selectable during loading #3739
Description
Please describe your proposal in a ONE sentence
WD profile can be selected in the "Load" dialog. More utilization can be obtained, by also making WD semantics selectable.
Underlying problem
Changing requires changing the Taclet options. This requires re-loading of proofs, because the Taclet option are only known, after a KeYUserProblemFile has been read.
For WD profile, the selection of the WD semantics is a crucial aspect directly from the start. The WD semantics are defined in optionsDeclarations.
A general approach
key.core.*should be free of UI stuff. Therefore, we need a dynamic way that we can determine an additional supplier of UI elements.- The UI elements, e.g. in this case provide the combobox for the selection of WD semantics.
- Somehow in a dynamical fashion these information are delivered to a method in the profile, which configures the
InitConfig. This may require re-checking the reusability of an existing profile.
Alternatives
Reloading of proofs.
Estimated effort
3h