Skip to content

Boxed Comments

Federico Ponzi edited this page Oct 19, 2024 · 2 revisions

this page was moved to https://docs.tlapl.us/using:vscode:boxed_comments


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