Unique colors for multi- and single-line comments

[lemmy]

The Toolbox colors multi-line (* *) and single-line * comments differently. I find this useful because it makes me use the former for actual documentation while the latter is used for spec notes/hints.

[alygin]

In VS Code, code highlighting works this way:

1. As an extension author, I define rules that assign scopes to various pieces of code. For instance, the extension now assigns the standard comment.block and comment.line scopes to block- and line-comments respectively (you can check this by running the "Inspect TM Scopes" and pointing to a comment).
2. There're many color theme extensions that provide rules on what color and font decorations are assigned to those scopes.
3. The user selects a color theme to her liking, so the code becomes highlighted in accordance with the rules from the theme.

So, at the moment, it's not up to me to decide what color will be used to decorate comments. Unfortunately, all the color themes I know use the same color for both block- and line-comments. But there're plenty of them, maybe there's a suitable one.

VS Code also provides the possibility for the user to change color for a given scope by manually editing the settings.json file, but unfortunately, it also doesn't recognise difference between block- and line-comments, it only supports the comments scope.

I was thinking of implementing a special color theme (or a set of themes) that would properly handle TLA+ token types, but there must be a better support for semantic coloring in VS Code (work in progress).

[alygin]

Recent progress on the VS Code side: https://github.com/microsoft/vscode/wiki/Semantic-Highlighting-Overview

[will62794]

On a related note, would it be possible to add functionality for formatting block comments in the same way that the Toolbox allows? e.g.

(***************************************************************************)
(* The following lemma is an immediate consequence of the assumption.      *)
(***************************************************************************)

[alygin]

If you mean the Toolbox comment-related commands like "Start boxed comment" "Box comment", "Format and box" etc, then yes, it can be implemented via custom commands.

[lemmy]

FWIW: Consider pushing the Toolbox's functionality into tla2tools.jar to make it standalone and usable by the VSCode extension.