[Checkers] Spaces in commented JSR 308 annotations

[Michael Ernst]

Adam-

> Why not have the compiler always  recognize the annotations? That is,
> why would I not always want to use the option?

It's funny you should ask.  I wrote an explanation in the manual, but then
commented it out because I wanted to keep the manual short.  

This feature prevents the compiler from interpreting too many comments as
annotations, since some comments that start with @ may not be annotations.
For example, I've had trouble with pre-existing comments of the form "@
symbolname" in JML-annotated code.

                    -Mike