PlusCal syntax highlighting breaks if --algorithm is not on line of open comment

[dricketts]

This is extremely minor, but maybe worth noting in a wiki page. PlusCal syntax highlighting won't work if the algorithm is written as:

(*
--algorithm WriteStealing
{
{
    skip;
}
}
*)

However, it does work if the algorithm is written as:

(*--algorithm WriteStealing
{
{
    skip;
}
}
*)

[alygin]

You're right, in a couple of cases the extension doesn't capture boundaries of a PlusCal algorithm correctly. There's a quick fix for this particular issue, but unfortunately, it brings other highlighting problems. VS Code has some limitations on grammar parsing, especially when it comes to embedded languages (PlusCal inside TLA+).

So, for the time being, I'll leave the highlighting rules as they are. But I'll add some kind of Caveats section to the Wiki. Thanks for the idea!

[alygin]

Here it is: Caveats

[dricketts]

Thanks, that looks good to me.

[alygin]

There's an attempt to improve VS Code highlighting capabilities: https://github.com/microsoft/vscode/issues/77133. I hope the result will allow us to fix this issue.

[alygin]

BTW, it's also better to keep the closing curly bracket on the last comment line:

(*--algorithm WriteStealing {
{
    skip;
}
} *)

The extension starting with version 1.2 handles it better.

[lemmy]

A similar problem if opening bracket of define is on the next line:

define
{
   ...
}

See https://github.com/lemmy/azure-cosmos-tla/blob/6e4e505a663ced50a61120219a70c7a2c1ae0f17/general-model/cosmos_client.tla#L84-L85