Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Correctly colour nested comments in VDM editor #775

Open
nickbattle opened this issue Feb 5, 2021 · 1 comment
Open

Correctly colour nested comments in VDM editor #775

nickbattle opened this issue Feb 5, 2021 · 1 comment
Labels
enhancement Not a bug, but nice to have

Comments

@nickbattle
Copy link
Contributor

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.

@nickbattle nickbattle added the enhancement Not a bug, but nice to have label Feb 5, 2021
@nickbattle
Copy link
Contributor Author

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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement Not a bug, but nice to have
Projects
None yet
Development

No branches or pull requests

1 participant