Gary T. Leavens
-
2005-09-29
- assigned_to: cheon --> nobody
Beginners should receive a warning when they write a
comment such as
// @ ...
or
/* @ ... */
which causes both JML and Java to ignore the text.
That is, we should change the lexer so that, at the start
of a comment, after several white space characters, if
the first character is an at-sign (@) then a warning is
issued.
This warning should be able to be disabled by a
command line switch, but the default should be to give
the warning and to have it appear.