Skip to content

Correctly colour nested comments in VDM editor #775

@nickbattle

Description

@nickbattle

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNot a bug, but nice to have

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions