Closed pmer closed 7 years ago
The grammar for TLA+ is defined in page 276 (PDF page 294) of Specifying Systems.
The formal grammar of PlusCal is defined in page 57 (PDF page 60) of A PlusCal User’s Manual C-Syntax∗ Version 1.8.
Documentation on TextMate language grammar specification is at https://manual.macromates.com/en/language_grammars.
The TLA+/C-style PlusCal/P-style PlusCal grammars that are used in the Toolbox is described in TokenizeSpec.java. Maybe this can tell us how to implement the VS Code grammar correctly for colorizing.
We're running into trouble making PlusCal programs looks different from TLA+ comments.
Let's try coloring everything in PlusCal programs.
Goal: Having it look like the TLA+ Toolbox and not be a completely separate color.
Grammar (syntax highlighting)
Grammars have two parts:
A configuration file "./language-configuration.json" in our extension. It teaches VS Code what TLA+ comments and string are. (Wait, does TLA+ have strings?)
A TextMate grammar for the language. Maybe agentultra/TLAGrammar? Looks like the same highlighter that GitHub uses when coloring TLA+ files. It lacks support for highlighting PlusCal expressions inside comments.
Also, just for fun, check this out for a read about the complexity of TLA+ grammars. It's a reminder that TLA+ expressions are even more whitespace-dependent for semantics than Python.