Problem description:
If "test" is used in Submission.thy we get surprising errors.
Example (Submission.thy):
...
lemma test: True
by simp
...
Output:
...
Draft.Submission | Outer syntax error\<^here>: proposition expected, but end-of-input\<^here> was found
-- | --
Draft.Submission | Outer syntax error\<^here>: term expected, but keyword :\<^here> was found
Draft.Submission | Bad context for command "apply"\<^here> -- using reset state
...
Expected behavior: The system should accept the submission.
Analysis:
In OK_Test.thy, we define the command test and thus reserve it as a keyword.
Solution proposals:
Warn user if "test" is used as an identifier
Find a less common name, and hope it will not be used
Find a way to register the command in the proper context but to bind the command only later. This would also be the preferred solution for other commands defined in OK_Test.thy.
Problem description: If "test" is used in
Submission.thywe get surprising errors.Example (
Submission.thy):Output:
Expected behavior: The system should accept the submission.
Analysis: In
OK_Test.thy, we define the commandtestand thus reserve it as a keyword.Solution proposals:
OK_Test.thy.