When a file directly starts with a TLA+ keyword or operator, the text zone before the beginning of the module -------- MODULE modulename -------- is not highlighted as a comment region as it should be but as regular TLA+ code instead.
keyword random text causes the issuekeyword random text does not (because of the whitespece)keywordrandom text does not (not a keyword)
When a file directly starts with a TLA+ keyword or operator, the text zone before the beginning of the module
-------- MODULE modulename --------is not highlighted as a comment region as it should be but as regular TLA+ code instead.keyword random textcauses the issuekeyword random textdoes not (because of the whitespece)keywordrandom textdoes not (not a keyword)