Skip to content

Boxed Comments

Andrew Lygin edited this page Mar 21, 2021 · 2 revisions

It's a common practice to use boxed comments in TLA+ specifications:

(**************************************************************)
(* This is a boxed comment.                                   *)
(* Such comment format is used in lots of specifications.     *)
(**************************************************************)

If you'd like to format your comments this way easily, you might want to install the Comment Box extension, and add the following settings to your settings.json:

"commentBox.styles": {
    "defaultStyle": {
        "commentStartToken": "(**",
        "commentEndToken": "**)",
        "leftEdgeToken": "(* ",
        "rightEdgeToken": " *)",
        "topEdgeToken": "*",
        "bottomEdgeToken": "*",
        "topRightToken": "**)",
        "bottomLeftToken": "(**",
        "capitalize": false,
        "ignoreInnerIndentation": false,
        "ignoreOuterIndentation": false,
        "removeEmptyLines": false,
        "textAlignment": "left"
    }
}

You can add multiple styles with different settings, add shortcuts to quickly apply formatting, etc. Please, refer to the Comment Box documentation for the full feature list.

Clone this wiki locally