Markus Alexander Kuppe

> I went to go update the Wiki; I think maybe I need to be a contributor to do so? You should have received an invite to join the project.

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

Related: https://github.com/alygin/vscode-tlaplus/issues/218

The work as part of https://github.com/alygin/vscode-tlaplus/issues/242 identified/created the problem that the code can check another specification than what the HTML page shows.

Here is a high-level description of what is needed: Must --- - Extension settings to set tlapm path - Invoke tlapm from vscode extension - Parse tlapm output and annotate...

@dricketts It occurred to me that I would find it useful if all facts were visually annotated in the module that appear in the ```BY DEF``` statements of the current...

It would annotate the *definition* of `Lemma1` and `Foo` where they appear in the spec.

IIRC the proof coloring is exclusively implemented in the Toolbox. The same goes for the proof decomposition functionality. Perhaps more of this functionality should be moved out of the Toolbox...

@xosmig What is your locale?

I suppose we could remove the formatting when TLC runs with the `-tool` flag. However, it would be inconsistent to still format dates according to the locale. At any rate,...