Repository navigation
Correctly colour nested comments in VDM editor #775
Description
This change is linked to issue #774, enabling nested comments.
If #774 is accepted, the editor ought to change to correctly colour-code a nested comment. Without such a change, the parser understands that a larger block (typically) is being commented out, but does not correctly colour the whole comment.
Activity
nickbattle commentedon May 3, 2021
After discussions in the Language Board (overturetool/language#52), this change will go ahead, though with the default/-strict behaviour being as it currently is. A new entry in Properties.java is used to control the nested comment parsing required, so this ought really to be available in the project settings somewhere.
Currently, it looks like the generated/vdmj.properties file that is created from a launch configuration does not get loaded when the editor is parsing a file. eg. in ide/parsers/vdmj/src/main/java/org/overture/ide/parsers/vdmj/SourceParserVdmSl.java. The Properties.init() call is made, but the vdmj.properties file is not on the classpath at this point, so the defaults apply. This suggests we need an "editor properties" file as well as the "generated" one for runtime.
@idhugoid would that be a simple change?