Error handling when command not applicable
If a script command is not applicable KeY raises a Script Exception. We have two choices to handle that:
- If a command is not applicable the script execution stops with the marker and the current state is presented to the user
- We skip this command an further execute the script. But we identify the user with a warning message
I prefer the first version as long as the command is not in an isClosable Statement.
To upload designs, you'll need to enable LFS. More information