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 and have an admin enable hashed storage. More information